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
• Counterexample guided path reduction for static program analysis
• Mind the gap: bit-vector interpolation recast over linear integer arithmetic
• Software model checking with explicit scheduler and symbolic threads
• An automatic method for the dynamic construction of abstractions of states of a formal model
• Cardinality Abstraction for Declarative Networking Applications
• Highly dependable concurrent programming using design for verification
• Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
• Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
• Rule-based static analysis of network protocol implementations
• Backward symbolic execution with loop folding
• Predicate Abstraction of Programs with Non-linear Computation
• Abstraction and abstraction refinement
• 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
• Verifying parallel algorithms and programs using coloured Petri nets
• 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
• A traversal-based algorithm for higher-order model checking
• System-level state equality detection for the formal dynamic verification of legacy distributed applications
• Automated inference of library specifications for source-sink property verification
• Stochastic modelling of communication protocols from source code
• Automatic modular abstractions for template numerical constraints
• Lazy abstraction-based controller synthesis
• Connecting program synthesis and reachability: automatic program repair using test-input generation
• 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
• 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
• TRACER: a symbolic execution tool for verification
• Model Checking Software
• Competent predicate abstraction in model checking
• Computer Aided Verification
• Static Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• Splitting via Interpolants
• Symbolic computation via program transformation
• Whale: an interpolation-based algorithm for inter-procedural verification
• A generic framework for heap and value analyses of object-oriented programming languages
• Interpolant Generation for UTVPI
• Collaborative verification and testing with explicit assumptions
• A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes
• From invariant checking to invariant inference using randomized search
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Program analysis with local policy iteration
• Craig interpolation in the presence of non-linear constraints
• Efficient interpolation for the theory of arrays
• Compositional Predicate Abstraction from Game Semantics
• Computer Aided Verification
• A model checking-based approach for security policy verification of mobile systems
• 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
• Model Checking Software
• An invariant-based approach to the verification of asynchronous parameterized networks
• Model Checking Software
• High-order curvilinear finite elements for axisymmetric Lagrangian hydrodynamics
• Sets with cardinality constraints in satisfiability modulo theories
• 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
• Information reuse for multi-goal reachability analyses
• Proving Termination of Tree Manipulating Programs
• Theory and practice of unparsed patterns for metacompilation
• Integrating topological proofs with model checking to instrument iterative design
• CPBPV: a constraint-programming framework for bounded program verification
• Programming Languages and Systems
• Combining model checking and data-flow analysis
• An interpolating theorem prover
• Hybrid Systems: Computation and Control
• Computer Aided Verification
• Static Analysis
• MLAT: a tool for heap analysis based on predicate abstraction by modal logic
• Incremental false path elimination for static software analysis
• A unifying view on SMT-based software verification
• Thread-modular abstraction refinement.
• From under-approximations to over-approximations and back

This page was built for software: BLAST