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

DOI10.1007/978-3-030-81685-8_32MaRDI QIDQ832220zbMATH OpenOpenAlexFDO

Authors Guillaume Girol, Benjamin Farinier, Sébastien Bardin

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

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

Recommendations

• Correct Hardware Design and Verification Methods
• Feasibility analysis for robustness quantification by symbolic model checking
• A formal model for detecting bugs by symbolic execution of programs
• Formal Methods in Computer-Aided Design
• Robust reachability in timed automata: a game-based approach

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3776831 (Why is no real title available?)
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• A logic for reasoning about time and reliability
• Arrays made simpler: an efficient, scalable and thorough preprocessing
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Efficient CTL model-checking for pushdown systems
• Efficient E-Matching for SMT Solvers
• Information theory and security: Quantitative information flow
• Model counting: a new stategy for obtaining good bounds
• Model generation for quantified formulas: a taint-based approach
• Termination of Probabilistic Concurrent Program
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation

Cited in

(2)

• Adversarial reachability for program-level security analysis
• Preface of the special issue on the conference on computer-aided verification 2020 and 2021

Describes a project that uses

Uses Software

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

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

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