Not all bugs are created equal, but robust reachability can tell the difference

DOI10.1007/978-3-030-81685-8_32zbMath1493.68109OpenAlexW3187071876MaRDI QIDQ832220

Guillaume Girol, Sébastien Bardin, Benjamin Farinier

Publication date: 25 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81685-8_32

Mathematics Subject Classification ID

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

Uses Software

• CUTE
• NuSMV
• z3
• PathCrawler
• DART
• CVC4
• CBMC
• BINSEC/SE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Efficient CTL model-checking for pushdown systems
• A logic for reasoning about time and reliability
• Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
• Information Theory and Security: Quantitative Information Flow
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Termination of Probabilistic Concurrent Program
• Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Model generation for quantified formulas: a taint-based approach

This page was built for publication: Not all bugs are created equal, but robust reachability can tell the difference