Automated formal analysis and verification: an overview
From MaRDI portal
Publication:2871577
DOI10.1080/03081079.2012.757437zbMath1286.68318OpenAlexW1987328668MaRDI QIDQ2871577
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Model-checking in dense real-time
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Results on the propositional \(\mu\)-calculus
- Symbolic model checking: \(10^{20}\) states and beyond
- Monotone data flow analysis frameworks
- A theory of timed automata
- Symbolic model checking for real-time systems
- Using partial orders for the efficient verification of deadlock freedom and safety properties
- Introduction to set constraint-based program analysis
- Process rewrite systems.
- Pushdown processes: Games and model-checking
- A structural induction theorem for processes
- Unreliable channels are easier to verify than perfect channels
- Verifying programs with unreliable channels
- Forest automata for verification of heap manipulation
- Verification of parametric concurrent systems with prioritised FIFO resource management
- New Developments in WCET Analysis
- Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
- Graph-Based Algorithms for Boolean Function Manipulation
- “Sometimes” and “not never” revisited
- Global Data Flow Analysis and Iterative Algorithms
- Reasoning about systems with many processes
- Model checking the full modal mu-calculus for infinite sequential processes
- Lazy abstraction
- Transition predicate abstraction and fair termination
- Efficient Runtime Detection and Toleration of Asymmetric Races
- Abstract Interpretation Frameworks
- Computer Science Logic
- CONCUR 2004 - Concurrency Theory
- Computer Aided Verification
- Automata-Theoretic Model Checking Revisited
- Formal Methods for the Design of Real-Time Systems
- An axiomatic basis for computer programming
- A machine program for theorem-proving
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- CONCUR 2005 – Concurrency Theory
- Computer Aided Verification
- Symbolic model checking with rich assertional languages
- Automatic verification of parameterized networks of processes
This page was built for publication: Automated formal analysis and verification: an overview
