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)

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

Describes a project that uses

Uses Software

• NModel
• AsmL
• Boogie
• z3

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)