CPBPV: a constraint-programming framework for bounded program verification

DOI10.1007/S10601-009-9089-9MaRDI QIDQ968353zbMATHOpenAlexFDO

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

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

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

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1975609
• Program verification using constraint handling rules and array constraint generalizations

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 4162324 (Why is no real title available?)
• scientific article; zbMATH DE number 1956607 (Why is no real title available?)
• scientific article; zbMATH DE number 1406234 (Why is no real title available?)
• Abstraction Refinement of Linear Programs with Arrays
• Automatic software model checking via constraint logic
• Bounded model checking using satisfiability solving
• CPBPV: a constraint-programming framework for bounded program verification
• Challenges in Satisfiability Modulo Theories
• Computer Aided Verification
• Efficient SAT-based bounded model checking for software verification
• Model Checking Software
• Model Checking Software
• Predicate abstraction of ANSI-C programs using SAT
• Test Data Generation of Bytecode by CLP Partial Evaluation
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(3)

• CPBPV: a constraint-programming framework for bounded program verification
• Tools and Algorithms for the Construction and Analysis of Systems
• CPBPV

Describes a project that uses

Uses Software

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

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

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