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

DOI10.1007/978-3-319-49815-7_12zbMATH Open1396.68036OpenAlexW2553899165MaRDI QIDQ1784791FDOQ1784791

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

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.

Mathematics Subject Classification ID

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

Cited In (4)

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

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)