CPBPV: a constraint-programming framework for bounded program verification

DOI10.1007/s10601-009-9089-9zbMath1213.68173OpenAlexW2604202109MaRDI QIDQ968353

Pascal Van Hentenryck, Michel Rueher, Hélène Collavizza

Publication date: 5 May 2010

Published in: Constraints (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10601-009-9089-9

zbMATH Keywords

bounded program verificationconstraint-based symbolic executiondetection of nonconformitiestest cases generation

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17)

Related Items (2)

CPBPV: a constraint-programming framework for bounded program verification ⋮ CPBPV

Uses Software

• BLAST
• KRAKATOA
• SPIN
• Why3
• JML
• Caduceus
• Bebop
• CBMC
• SatAbs
• Numerica

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Efficient SAT-based bounded model checking for software verification
• CPBPV: a constraint-programming framework for bounded program verification
• Automatic software model checking via constraint logic
• Predicate abstraction of ANSI-C programs using SAT
• Test Data Generation of Bytecode by CLP Partial Evaluation
• Model Checking Software
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Challenges in Satisfiability Modulo Theories
• Tools and Algorithms for the Construction and Analysis of Systems
• Abstraction Refinement of Linear Programs with Arrays
• Model Checking Software
• Tools and Algorithms for the Construction and Analysis of Systems
• Bounded model checking using satisfiability solving

This page was built for publication: CPBPV: a constraint-programming framework for bounded program verification