BLAST
From MaRDI portal
Software:15473
swMATH2937MaRDI QIDQ15473FDOQ15473
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Efficient strategies for CEGAR-based model checking
- Automated Inference of Library Specifications for Source-Sink Property Verification
- Software model checking with explicit scheduler and symbolic threads
- An automatic method for the dynamic construction of abstractions of states of a formal model
- Lazy Abstraction-Based Controller Synthesis
- Cardinality Abstraction for Declarative Networking Applications
- Verifying Parallel Algorithms and Programs Using Coloured Petri Nets
- Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation
- Automatic Modular Abstractions for Template Numerical Constraints
- Highly dependable concurrent programming using design for verification
- Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
- Rule-based static analysis of network protocol implementations
- Backward symbolic execution with loop folding
- Predicate Abstraction of Programs with Non-linear Computation
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- Inductive Decidability Using Implicit Induction
- Abstraction refinement and antichains for trace inclusion of infinite state systems
- A compositional behavioral modeling framework for embedded system design and conformance checking
- Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
- Infeasible Paths Elimination by Symbolic Execution Techniques
- Counterexample Guided Path Reduction for Static Program Analysis
- Heuristic Search for the Analysis of Graph Transition Systems
- Boosting Lazy Abstraction for SystemC with Partial Order Reduction
- Automatically verifying temporal properties of pointer programs with cyclic proof
- Predicate Abstraction in Program Verification: Survey and Current Trends
- Abstraction and Abstraction Refinement
- A traversal-based algorithm for higher-order model checking
- System-level state equality detection for the formal dynamic verification of legacy distributed applications
- Stochastic modelling of communication protocols from source code
- Title not available (Why is that?)
- Verify heaps via unified model checking
- Verifying Reference Counting Implementations
- Fixpoint-Guided Abstraction Refinements
- Integration of a Software Model Checker into Isabelle
- LMS-Verify: abstraction without regret for verified systems programming
- Combining Model Checking and Data-Flow Analysis
- EUFORIA: complete software model checking with uninterpreted functions
- Translating Xd-C programs to MSVL programs
- Query-Driven Program Testing
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Model-checking structured context-free languages
- Wombit: a portfolio bit-vector solver using word-level propagation
- Model checking dynamic memory allocation in operating systems
- Automation of broad sanity test generation
- Towards Automatic Stability Analysis for Rely-Guarantee Proofs
- Model Checking Software
- Competent predicate abstraction in model checking
- Computer Aided Verification
- Computer Aided Verification
- Static Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- Splitting via Interpolants
- From Under-Approximations to Over-Approximations and Back
- Symbolic computation via program transformation
- A generic framework for heap and value analyses of object-oriented programming languages
- Interpolant Generation for UTVPI
- From invariant checking to invariant inference using randomized search
- Formal verification of C systems code. Structured types, separation logic and theorem proving
- Efficient interpolation for the theory of arrays
- Compositional Predicate Abstraction from Game Semantics
- Computer Aided Verification
- Incremental False Path Elimination for Static Software Analysis
- A model checking-based approach for security policy verification of mobile systems
- Integrating Topological Proofs with Model Checking to Instrument Iterative Design
- An extension of lazy abstraction with interpolation for programs with arrays
- Experience of improving the BLAST static verification tool
- Automated formal analysis and verification: an overview
- Automatically verifying temporal properties of pointer programs with cyclic proof
- Verification: Theory and Practice
- Temporal property verification as a program analysis task
- Information Reuse for Multi-goal Reachability Analyses
- Model Checking Software
- TRACER: A Symbolic Execution Tool for Verification
- An invariant-based approach to the verification of asynchronous parameterized networks
- Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
- Program Analysis with Local Policy Iteration
- Model Checking Software
- Title not available (Why is that?)
- A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes
- High-order curvilinear finite elements for axisymmetric Lagrangian hydrodynamics
- Craig Interpolation in the Presence of Non-linear Constraints
- Explicit State Model Checking for Graph Grammars
- Slicing Abstractions
- Abstraction Refinement of Linear Programs with Arrays
- Automatic analysis of DMA races using model checking and \(k\)-induction
- Doomed program points
- Dual analysis for proving safety and finding bugs
- Integration of verification methods for program systems
- Proving Termination of Tree Manipulating Programs
- Theory and practice of unparsed patterns for metacompilation
- CPBPV: a constraint-programming framework for bounded program verification
- Programming Languages and Systems
- An interpolating theorem prover
- Collaborative Verification and Testing with Explicit Assumptions
- Hybrid Systems: Computation and Control
- Computer Aided Verification
- Static Analysis
- A unifying view on SMT-based software verification
- Sets with Cardinality Constraints in Satisfiability Modulo Theories
This page was built for software: BLAST