Boolean and Cartesian Abstraction for Model Checking C Programs
- 23 March 2001
- conference paper
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 268-283
- https://doi.org/10.1007/3-540-45319-9_19
Abstract
No abstract availableThis publication has 19 references indexed in Scilit:
- Design and synthesis of synchronization skeletons using branching time temporal logicPublished by Springer Science and Business Media LLC ,2005
- Automatic predicate abstraction of C programsPublished by Association for Computing Machinery (ACM) ,2001
- Making abstract interpretations completeJournal of the ACM, 2000
- Bebop: A Symbolic Model Checker for Boolean ProgramsLecture Notes in Computer Science, 2000
- Counterexample-Guided Abstraction RefinementLecture Notes in Computer Science, 2000
- Experience with Predicate AbstractionLecture Notes in Computer Science, 1999
- Formal language, grammar and set-constraint-based program analysis by abstract interpretationPublished by Association for Computing Machinery (ACM) ,1995
- Optimality in abstractions of model checkingLecture Notes in Computer Science, 1995
- Model checking and abstractionPublished by Association for Computing Machinery (ACM) ,1992
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977