μz- an efficient engine for fixed points with constraints

Krystof Hoder; Kryštof Hoder; Nikolaj Bjørner; Leonardo De Moura

doi:10.1007/978-3-642-22110-1_36

μz- an efficient engine for fixed points with constraints

Krystof Hoder, Kryštof Hoder, Nikolaj Bjørner, Leonardo De Moura

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

Abstract

The μZ tool is a scalable, efficient engine for fixed points with constraints. It supports high-level declarative fixed point constraints over a combination of built-in and plugin domains. The built-in domains include formulas presented to the SMT solver Z3 and domains known from abstract interpretation. We present the interface to μZ, a number of the domains, and a set of examples illustrating the use of μZ. © 2011 Springer-Verlag.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Pages	457-462
Number of pages	5
Volume	6806
DOIs	https://doi.org/10.1007/978-3-642-22110-1_36
Publication status	Published - 2011
Event	23rd International Conference on Computer Aided Verification, CAV 2011 - Snowbird, UT Duration: 1 Jul 2011 → …

Conference

Conference	23rd International Conference on Computer Aided Verification, CAV 2011
City	Snowbird, UT
Period	1/07/11 → …

Access to Document

10.1007/978-3-642-22110-1_36

Cite this

@inproceedings{57d06a4c4a0e473787bf07215a848810,

title = "μz- an efficient engine for fixed points with constraints",

abstract = "The μZ tool is a scalable, efficient engine for fixed points with constraints. It supports high-level declarative fixed point constraints over a combination of built-in and plugin domains. The built-in domains include formulas presented to the SMT solver Z3 and domains known from abstract interpretation. We present the interface to μZ, a number of the domains, and a set of examples illustrating the use of μZ. {\textcopyright} 2011 Springer-Verlag.",

author = "Krystof Hoder and Kry{\v s}tof Hoder and Nikolaj Bj{\o}rner and {De Moura}, Leonardo",

year = "2011",

doi = "10.1007/978-3-642-22110-1_36",

language = "English",

isbn = "9783642221095",

volume = "6806",

pages = "457--462",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

note = "23rd International Conference on Computer Aided Verification, CAV 2011 ; Conference date: 01-07-2011",

}

Hoder, K, Hoder, K, Bjørner, N & De Moura, L 2011, μz- an efficient engine for fixed points with constraints. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 6806, pp. 457-462, 23rd International Conference on Computer Aided Verification, CAV 2011, Snowbird, UT, 1/07/11. https://doi.org/10.1007/978-3-642-22110-1_36

μz- an efficient engine for fixed points with constraints. / Hoder, Krystof; Hoder, Kryštof; Bjørner, Nikolaj et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 6806 2011. p. 457-462.

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - μz- an efficient engine for fixed points with constraints

AU - Hoder, Krystof

AU - Hoder, Kryštof

AU - Bjørner, Nikolaj

AU - De Moura, Leonardo

PY - 2011

Y1 - 2011

N2 - The μZ tool is a scalable, efficient engine for fixed points with constraints. It supports high-level declarative fixed point constraints over a combination of built-in and plugin domains. The built-in domains include formulas presented to the SMT solver Z3 and domains known from abstract interpretation. We present the interface to μZ, a number of the domains, and a set of examples illustrating the use of μZ. © 2011 Springer-Verlag.

AB - The μZ tool is a scalable, efficient engine for fixed points with constraints. It supports high-level declarative fixed point constraints over a combination of built-in and plugin domains. The built-in domains include formulas presented to the SMT solver Z3 and domains known from abstract interpretation. We present the interface to μZ, a number of the domains, and a set of examples illustrating the use of μZ. © 2011 Springer-Verlag.

U2 - 10.1007/978-3-642-22110-1_36

DO - 10.1007/978-3-642-22110-1_36

M3 - Conference contribution

SN - 9783642221095

VL - 6806

SP - 457

EP - 462

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

T2 - 23rd International Conference on Computer Aided Verification, CAV 2011

Y2 - 1 July 2011

ER -

μz- an efficient engine for fixed points with constraints

Abstract

Conference

Access to Document

Fingerprint

Cite this