SLAM

swMATH3136MaRDI QIDQ15668

No author found.

Related Items (only showing first 100 items - show all)

Software Verification with PDR: An Implementation of the State of the Art ⋮ ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ⋮ Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ Splitting via Interpolants ⋮ From Under-Approximations to Over-Approximations and Back ⋮ Modular strategies for recursive game graphs ⋮ Specification and Verification of Multi-Agent Systems ⋮ A Lightweight Approach for Loop Summarization ⋮ SAT-Based Model Checking ⋮ Abstraction and Abstraction Refinement ⋮ Predicate Abstraction for Program Verification ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Model Checking Procedural Programs ⋮ Combining Model Checking and Testing ⋮ Transfer of Model Checking to Industrial Practice ⋮ Taking Satisfiability to the Next Level with Z3 ⋮ Winning Regions of Pushdown Parity Games: A Saturation Method ⋮ Unnamed Item ⋮ Verification: Theory and Practice ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Predicate diagrams for the verification of real-time systems ⋮ Highly dependable concurrent programming using design for verification ⋮ Unnamed Item ⋮ CONCUR 2004 - Concurrency Theory ⋮ An integrated approach to high integrity software verification ⋮ Data structures for symbolic multi-valued model-checking ⋮ Unnamed Item ⋮ Toward compositional verification of interruptible OS kernels and device drivers ⋮ Unnamed Item ⋮ Runtime Verification Based on Register Automata ⋮ Context-aware counter abstraction ⋮ Automated Inference of Library Specifications for Source-Sink Property Verification ⋮ System-level state equality detection for the formal dynamic verification of legacy distributed applications ⋮ C-SHORe ⋮ Proving Termination of Tree Manipulating Programs ⋮ Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction ⋮ A model checking-based approach for security policy verification of mobile systems ⋮ A unifying view on SMT-based software verification ⋮ On the Satisfiability of Modular Arithmetic Formulae ⋮ Efficient strategies for CEGAR-based model checking ⋮ A divide-and-conquer approach for analysing overlaid data structures ⋮ Counterexample-guided abstraction refinement for symmetric concurrent programs ⋮ Model checking RAISE applicative specifications ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Predicate extension of symbolic memory graphs for the analysis of memory safety correctness ⋮ An Introduction to Practical Formal Methods Using Temporal Logic ⋮ Monitoring and recovery for web service applications ⋮ A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes ⋮ Compositionality Entails Sequentializability ⋮ Model Checking Higher-Order Programs ⋮ Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation ⋮ Fluid Updates: Beyond Strong vs. Weak Updates ⋮ On model checking multiple hybrid views ⋮ Verify heaps via unified model checking ⋮ Verifying Parallel Algorithms and Programs Using Coloured Petri Nets ⋮ Horn clause verification with convex polyhedral abstraction and tree automata-based refinement ⋮ Automatic Termination Verification for Higher-Order Functional Programs ⋮ Loop summarization using state and transition invariants ⋮ Correctness kernels of abstract interpretations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A saturation method for the modal \(\mu \)-calculus over pushdown systems ⋮ Rule-based static analysis of network protocol implementations ⋮ Computer aided verification. 16th international conference, CAV 2004, Boston, MA, USA, July 13--17, 2004. Proceedings. ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ DKAL and Z3: A Logic Embedding Experiment ⋮ Automatic decidability and combinability ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Software Model Checking: Searching for Computations in the Abstract or the Concrete ⋮ Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs ⋮ Solving games via three-valued abstraction refinement ⋮ Generating models of infinite-state communication protocols using regular inference with abstraction ⋮ A local approach for temporal model checking of Java bytecode ⋮ Embedded software verification using symbolic execution and uninterpreted functions ⋮ An Assume Guarantee Approach for Checking Quantified Array Assertions ⋮ Symmetry and Completeness in the Analysis of Parameterized Systems ⋮ EUFORIA: complete software model checking with uninterpreted functions ⋮ Verifying Reference Counting Implementations ⋮ Refinement-Based CFG Reconstruction from Unstructured Programs ⋮ Abstraction Refinement for Quantified Array Assertions ⋮ Refinement of Trace Abstraction ⋮ Algorithmic Analysis of Array-Accessing Programs ⋮ Loop Invariants from Counterexamples ⋮ Refining abstract interpretations ⋮ Model Checking Software ⋮ Tools and Algorithms for the Construction and Analysis of Systems ⋮ Tools and Algorithms for the Construction and Analysis of Systems ⋮ Generalized Property Directed Reachability ⋮ Computer Aided Verification ⋮ Computer Aided Verification ⋮ Programming Languages and Systems ⋮ Establishing local temporal heap safety properties with applications to compile-time memory management ⋮ Dependent types from counterexamples ⋮ A semantic framework for the abstract model checking of tccp programs ⋮ A general framework for types in graph rewriting ⋮ Stochastic Modelling of Communication Protocols from Source Code ⋮ Automated formal analysis and verification: an overview ⋮ Behavioral interface specification languages

This page was built for software: SLAM