On Bounded Reachability of Programs with Set Comprehensions

DOI10.1007/978-3-540-89439-1_22MaRDI QIDQ5505562zbMATH OpenOpenAlexFDO

Authors Margus Veanes, Ando Saabas

Publication date 27 January 2009

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-89439-1_22

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Recommendations

• Reachability Analysis of Procedural Programs with Affine Integer Arithmetic
• Abstract domains and solvers for sets reasoning
• Reachability modulo theories
• Analyzing automata with Presburger arithmetic and uninterpreted function symbols
• On the complexity of set-based analysis

Cited in

(8)

• Automated reasoning with restricted intensional sets
• A coinductive approach to computing with compact sets
• Constraint-based reachability
• Abstract domains and solvers for sets reasoning
• On the convergence of query-bounded computations and logical closure properties of c.e. sets
• Reachability modulo theories
• Reachability Analysis of Procedural Programs with Affine Integer Arithmetic
• Composing model programs for analysis

Describes a project that uses

Uses Software

• z3
• Boogie
• AsmL
• NModel

This page was built for publication: On Bounded Reachability of Programs with Set Comprehensions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5505562)