Automated formal analysis and verification: an overview

DOI10.1080/03081079.2012.757437MaRDI QIDQ2871577zbMATH OpenOpenAlexFDO

Authors Bohuslav Křena, Tomáš Vojnar

Publication date 8 January 2014

Published in International Journal of General Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1080/03081079.2012.757437

zbMATH Keywords

formal analysis and verificationmodel checkingstate space explosionstatic analysistheorem proving

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

• scientific article; zbMATH DE number 1633145
• scientific article; zbMATH DE number 1746645
• scientific article; zbMATH DE number 1487860
• scientific article; zbMATH DE number 1538014
• Pragmatics of model checking: An STTT special section

Cites work

• A machine program for theorem-proving
• A structural induction theorem for processes
• A theory of timed automata
• Abstract Interpretation Frameworks
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• An axiomatic basis for computer programming
• Automata-Theoretic Model Checking Revisited
• Automatic verification of parameterized networks of processes
• Comparison of algorithms for checking emptiness on Büchi automata
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Computer Science Logic
• CONCUR 2004 - Concurrency Theory
• CONCUR 2005 – Concurrency Theory
• Efficient Runtime Detection and Toleration of Asymmetric Races
• Forest automata for verification of heap manipulation
• Formal Methods for the Design of Real-Time Systems
• Global Data Flow Analysis and Iterative Algorithms
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 1614699 (Why is no real title available?)
• scientific article; zbMATH DE number 1670563 (Why is no real title available?)
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1670780 (Why is no real title available?)
• scientific article; zbMATH DE number 1670785 (Why is no real title available?)
• scientific article; zbMATH DE number 1670786 (Why is no real title available?)
• scientific article; zbMATH DE number 1670791 (Why is no real title available?)
• scientific article; zbMATH DE number 1701752 (Why is no real title available?)
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 4180789 (Why is no real title available?)
• scientific article; zbMATH DE number 3919813 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 3485178 (Why is no real title available?)
• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• scientific article; zbMATH DE number 1982210 (Why is no real title available?)
• scientific article; zbMATH DE number 2080053 (Why is no real title available?)
• scientific article; zbMATH DE number 1927558 (Why is no real title available?)
• scientific article; zbMATH DE number 1538040 (Why is no real title available?)
• scientific article; zbMATH DE number 1798184 (Why is no real title available?)
• scientific article; zbMATH DE number 2161330 (Why is no real title available?)
• scientific article; zbMATH DE number 1929967 (Why is no real title available?)
• scientific article; zbMATH DE number 2206109 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Introduction to set constraint-based program analysis
• Iterating transducers in the large (extended abstract)
• Lazy abstraction
• Model checking the full modal mu-calculus for infinite sequential processes
• Model-checking in dense real-time
• Monotone data flow analysis frameworks
• New Developments in WCET Analysis
• Process rewrite systems.
• Pushdown processes: Games and model-checking
• Reasoning about systems with many processes
• Results on the propositional \(\mu\)-calculus
• Symbolic model checking for real-time systems
• Symbolic model checking with rich assertional languages
• Symbolic model checking: \(10^{20}\) states and beyond
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Transition predicate abstraction and fair termination
• Unreliable channels are easier to verify than perfect channels
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Verification of parametric concurrent systems with prioritised FIFO resource management
• Verifying programs with unreliable channels
• “Sometimes” and “not never” revisited

Cited in

(3)

• Fundamental results for learning deterministic extended finite state machines from queries
• Automatic verification of combined specifications: an overview
• Automated Technology for Verification and Analysis

Describes a project that uses

Uses Software

• PRISM
• ACL2
• Isabelle/HOL
• LTSmin
• SatAbs
• Goldilocks
• Apron
• BLAST
• VCC
• Uppaal
• MONA
• CESAR
• Wolverine
• Coq
• SLAM
• DiVinE
• NuSMV
• z3
• KLEE
• VS3
• CPAchecker
• ABC
• ANaConDA

This page was built for publication: Automated formal analysis and verification: an overview

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