A bounded model checker for three-valued abstractions of concurrent software systems

DOI10.1007/978-3-319-49815-7_12MaRDI QIDQ1784791zbMATH OpenOpenAlexFDO

Authors Nils Timm, Stefan Gruner, Matthias Harvey

Publication date 27 September 2018

Full work available at URL https://doi.org/10.1007/978-3-319-49815-7_12

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

• Computer Aided Verification
• Model checking of concurrent software systems via heuristic-guided SAT solving
• Bounded model checking of infinite state systems
• Bounded model checking using satisfiability solving
• Model checking: from hardware to software.

Cited in

(4)

• Compositional Verification and 3-Valued Abstractions Join Forces
• Constraint reusing and \(k\)-induction for three-valued bounded model checking
• Computer Aided Verification
• Property Driven Three-Valued Model Checking on Hybrid Automata

Describes a project that uses

Uses Software

• NuSMV
• Sat4j
• CBMC

This page was built for publication: A bounded model checker for three-valued abstractions of concurrent software systems

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