SLAM
From MaRDI portal
SLAM Q15668
Cited in
(only showing first 100 items - show all)- Connecting program synthesis and reachability: automatic program repair using test-input generation
- Loop Invariants from Counterexamples
- An introduction to practical formal methods using temporal logic
- Loop summarization using state and transition invariants
- Efficient strategies for CEGAR-based model checking
- Verify heaps via unified model checking
- Establishing local temporal heap safety properties with applications to compile-time memory management
- Verifying Reference Counting Implementations
- On the Satisfiability of Modular Arithmetic Formulae
- scientific article; zbMATH DE number 1953039 (Why is no real title available?)
- Computer Aided Verification
- scientific article; zbMATH DE number 1953032 (Why is no real title available?)
- scientific article; zbMATH DE number 1903350 (Why is no real title available?)
- EUFORIA: complete software model checking with uninterpreted functions
- A saturation method for the modal \(\mu \)-calculus over pushdown systems
- Formal analysis of hierarchical state machines
- Model Checking Software
- Splitting via Interpolants
- Verification, Model Checking, and Abstract Interpretation
- Solving games via three-valued abstraction refinement
- scientific article; zbMATH DE number 1979541 (Why is no real title available?)
- Static Analysis
- Static Analysis
- Taking satisfiability to the next level with Z3 (abstract)
- Programming Languages and Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Whale: an interpolation-based algorithm for inter-procedural verification
- scientific article; zbMATH DE number 1953037 (Why is no real title available?)
- Algorithmic Analysis of Array-Accessing Programs
- scientific article; zbMATH DE number 2177632 (Why is no real title available?)
- Abstraction Refinement for Quantified Array Assertions
- A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes
- Data structures for symbolic multi-valued model-checking
- Formal Methods for Components and Objects
- Computation engineering. Applied automata theory and logic.
- A model checking-based approach for security policy verification of mobile systems
- Model checking higher-order programs
- An extension of lazy abstraction with interpolation for programs with arrays
- An integrated approach to high integrity software verification
- Predicate abstraction for program verification
- Model checking procedural programs
- Computer Aided Verification
- Automatic decidability and combinability
- An automata-theoretic approach to infinite-state systems
- Automated formal analysis and verification: an overview
- A semantic framework for the abstract model checking of tccp programs
- Context-aware counter abstraction
- Highly dependable concurrent programming using design for verification
- Predicate diagrams for the verification of real-time systems
- Modular strategies for recursive game graphs
- Model Checking Software
- Dependent types from counterexamples
- Software verification with PDR: an implementation of the state of the art
- Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
- Generating models of infinite-state communication protocols using regular inference with abstraction
- Combining model checking and testing
- Transfer of model checking to industrial practice
- Rule-based static analysis of network protocol implementations
- A local approach for temporal model checking of Java bytecode
- Behavioral interface specification languages
- A divide-and-conquer approach for analysing overlaid data structures
- A general framework for types in graph rewriting
- DKAL and Z3: a logic embedding experiment
- Aligator
- CUTE
- MPI-CHECK
- TopSpin
- Cogent
- FocusCheck
- Zing
- Moby/DC
- jMoped
- Symstra
- DiVer
- veriSoft
- ConSpec
- CalFuzzer
- PiXL
- StEAM
- SyncGen
- SCTL-MUS
- ACSAR
- BLAST
- SPIN
- ARMC
- ISP
- Dagger
- Bogor
- TSPASS
- bv2epr
- Zap
- ADL
- ESC/Java
- DART
- LTSmin
- Cseq
- CPAchecker
- Predator
- ComFoRT
- UFO
This page was built for software: SLAM
