Tools and Algorithms for the Construction and Analysis of Systems
From MaRDI portal
(Redirected from Publication:5308405)
Tools and Algorithms for the Construction and Analysis of Systems (scientific article; zbMATH DE number 5196458)
Tools and Algorithms for the Construction and Analysis of Systems (scientific article; zbMATH DE number 5196458)
Recommendations
Cited in
(97)- Data compression for proof replay
- Lattice-based refinement in bounded model checking
- A compiler for MSVL and its applications
- VST-Floyd: a separation logic tool to verify correctness of C programs
- Incremental bounded model checking for embedded software
- On compiling Boolean circuits optimized for secure multi-party computation
- A unifying view on SMT-based software verification
- Sharpening constraint programming approaches for bit-vector theory
- A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
- Efficient bounded model checking of heap-manipulating programs using tight field bounds
- The \textsc{MergeSat} solver
- Verification by gambling on program slices
- Loop summarization using state and transition invariants
- Scalable and precise refinement of cache timing analysis via path-sensitive verification
- Automated formal synthesis of provably safe digital controllers for continuous plants
- Abstract semantic diffing of evolving concurrent programs
- System-level state equality detection for the formal dynamic verification of legacy distributed applications
- A taxonomy of exact methods for partial Max-SAT
- An automatic method for the dynamic construction of abstractions of states of a formal model
- A compositional behavioral modeling framework for embedded system design and conformance checking
- Embedded software verification using symbolic execution and uninterpreted functions
- SATenstein: automatically building local search SAT solvers from components
- scientific article; zbMATH DE number 1670556 (Why is no real title available?)
- CCA-secure keyed-fully homomorphic encryption
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Exploiting binary floating-point representations for constraint propagation
- Context-free ambiguity detection using multi-stack pushdown automata
- Deciding Bit-Vector Formulas with mcSAT
- Loop invariant symbolic execution for parallel programs
- Matching multiplications in bit-vector formulas
- Partitioned memory models for program analysis
- Sequentialization using timestamps
- Strengthening induction-based race checking with lightweight static analysis
- SAT-Based Model Checking
- Transfer of model checking to industrial practice
- LCTD: test-guided proofs for C programs on LLVM
- A new approach to partial MUS enumeration
- Inferring Congruence Equations Using SAT
- Loop Summarization Using Abstract Transformers
- Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
- Information theory and security: Quantitative information flow
- Finding and fixing faults
- Symbolic predictive analysis for concurrent programs
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- An extension of lazy abstraction with interpolation for programs with arrays
- Deciding floating-point logic with abstract conflict driven clause learning
- Budget-bounded model-checking pushdown systems
- The configurable SAT solver challenge (CSSC)
- On black-box optimization in divide-and-conquer SAT solving
- scientific article; zbMATH DE number 7199588 (Why is no real title available?)
- Finding Effective SAT Partitionings Via Black-Box Optimization
- SMT-based model checking for recursive programs
- Counterexample guided path reduction for static program analysis
- Proving safety with trace automata and bounded model checking
- Empirical software metrics for benchmarking of verification tools
- Extending Model Checking with Dynamic Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- From non-preemptive to preemptive scheduling using synchronization synthesis
- Transfer function synthesis without quantifier elimination
- Automatically verifying temporal properties of pointer programs with cyclic proof
- Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
- Upper bound computation of information leakages for unbounded recursion
- Bit-precise verification of discontinuity errors under fixed-point arithmetic
- SMT-based verification of program changes through summary repair
- Automated program repair using formal verification techniques
- Intuitive modelling and formal analysis of collective behaviour in foraging ants
- Symbolic encoding of LL(1) parsing and its applications
- Process algebras and flocks of birds
- Efficient modular SMT-based model checking of pointer programs
- Doomed program points
- Explaining Hyperproperty Violations
- Adversarial reachability for program-level security analysis
- Exploring formal methods for cryptographic hash function implementations
- From bounded checking to verification of equivalence via symbolic up-to techniques
- Maximizing branch coverage with constrained Horn clauses
- Towards efficient data-flow test data generation
- A bounded model checking technique for higher-order programs
- Symbolic execution game semantics
- Formal methods for mobile ad hoc networks: a survey
- Exact approaches for the diverse satisfiability problem
- Generating additional constraints in algebraic cryptanalysis using SAT oracles
- Inverting 29-step MD5 compression function via SAT
- Preimage attack on 5-round cryptographic hash function JH-256 via parallel SAT solver
- Interpolation and SAT-based model checking revisited: adoption to software verification
- When you have a fuzzer, everything looks like a reachability problem
- Optimal concolic dynamic partial order reduction
- Preimage attack on round-reduced Skein512-256 compression function using SAT solver
- ParSAT: parallel solving of floating-point satisfiability
- Under-approximating loops in C programs for fast counterexample detection
- Automatic analysis of DMA races using model checking and k-induction
- Quantifying software reliability via model-counting
- Verified cryptographic code for everybody
- Not all bugs are created equal, but robust reachability can tell the difference
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
- Why does Astrée scale up?
- Efficient SAT-based bounded model checking for software verification
- CPBPV: a constraint-programming framework for bounded program verification
This page was built for publication: Tools and Algorithms for the Construction and Analysis of Systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5308405)
