BLAST

swMATH2937MaRDI QIDQ15473FDOQ15473

Author name not available (Why is that?)

Described by source

• Static Analysis
• Unnamed Publication

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