Partial completeness of abstract fixpoint checking. (Invited paper)

DOI10.1007/3-540-44914-0_1MaRDI QIDQ4536712zbMATH OpenFDO

Authors Patrick Cousot

Publication date 28 July 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44914-0_1

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Making abstract interpretations complete
• Making abstract models complete
• scientific article; zbMATH DE number 1834576
• Programming Languages and Systems
• Fixpoint-Guided Abstraction Refinements

Cited in

(21)

• Lattice-based refinement in bounded model checking
• Fixed point guided abstraction refinement for alternating automata
• Generalized abstraction-refinement for game-based CTL lifted model checking
• Fixpoint-Guided Abstraction Refinements
• scientific article; zbMATH DE number 1953028 (Why is no real title available?)
• scientific article; zbMATH DE number 2080047 (Why is no real title available?)
• scientific article; zbMATH DE number 1834576 (Why is no real title available?)
• Fixed points and frontiers: a new perspective
• scientific article; zbMATH DE number 7559481 (Why is no real title available?)
• scientific article; zbMATH DE number 7559486 (Why is no real title available?)
• Sound up-to techniques and complete abstract domains
• Abstraction in fixpoint logic
• Making abstract interpretations complete
• Making abstract models complete
• Calculational design of a regular model checker by abstract interpretation
• Deciding program properties via complete abstractions on bounded domains
• Exploiting adjoints in property directed reachability analysis
• Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
• Adjointness in property directed reachability analysis
• Why does Astrée scale up?
• Partial model checking via abstract interpretation

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Partial completeness of abstract fixpoint checking. (Invited paper)

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