z3
From MaRDI portal
Z3
Cited in
(only showing first 100 items - show all)- Efficient E-Matching for SMT Solvers
- Fast debugging of PRISM models
- Symbolic memory with pointers
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- A constraint-based approach to solving games on infinite graphs
- Ensuring correctness of model transformations while remaining decidable
- Loop Invariants from Counterexamples
- Symbolic string transformations with regular lookahead and rollback
- \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
- Detection and exploitation of functional dependencies for model generation
- Integrating simplex with tableaux
- An assertional proof of the stability and correctness of Natural Mergesort
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Efficient strategies for CEGAR-based model checking
- A practical approach to model checking duration calculus using Presburger arithmetic
- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
- Counterexample-guided inductive synthesis for probabilistic systems
- An assertional proof of red-black trees using Dafny
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- Transfer function synthesis without quantifier elimination
- Multiphase until formulas over Markov reward models: an algebraic approach
- Verifying array manipulating programs with full-program induction
- Para-disagreement logics and their implementation through embedding in Coq and SMT
- SeLoger
- Minimal counterexamples for linear-time probabilistic verification
- Proving stabilization of biological systems
- Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- CompoSAT: specification-guided coverage for model finding
- Heaps and Data Structures: A Challenge for Automated Provers
- Combined task- and network-level scheduling for distributed time-triggered systems
- Inferring expected runtimes of probabilistic integer programs using expected sizes
- Modeling high school timetabling with bitvectors
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Extending Sledgehammer with SMT solvers
- Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Tuple interpretations for termination of term rewriting
- Verifying Whiley programs with Boogie
- An efficient subsumption test pipeline for BS(LRA) clauses
- CTL* model checking for data-aware dynamic systems with arithmetic
- Flexible proof production in an industrial-strength SMT solver
- Automatic complexity analysis of integer programs via triangular weakly non-linear loops
- Guiding an automated theorem prover with neural rewriting
- Reasoning about vectors using an SMT theory of sequences
- \textsc{LTL} falsification in infinite-state systems
- Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
- Model checking hyperproperties for Markov decision processes
- Satisfiability checking for mission-time \textsf{LTL} (MLTL)
- MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions
- Regression verification for unbalanced recursive functions
- Multi-dimensional interpretations for termination of term rewriting
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Optimization modulo non-linear arithmetic via incremental linearization
- Test generation from event system abstractions to cover their states and transitions
- Constraint-based relational verification
- Causality-based game solving
- ATLAS: automated amortised complexity analysis of self-adjusting data structures
- Counterexample-guided partial bounding for recursive function synthesis
- An SMT solver for regular expressions and linear arithmetic over string length
- Implicit semi-algebraic abstraction for polynomial dynamical systems
- \textsc{Diffy}: inductive reasoning of array programs using difference invariants
- Automatic generation and validation of instruction encoders and decoders
- Learning probabilistic termination proofs
- Enforcing almost-sure reachability in POMDPs
- Interpolation and model checking for nonlinear arithmetic
- Not all bugs are created equal, but robust reachability can tell the difference
- Quantifier simplification by unification in SMT
- Learning union of integer hypercubes with queries (with applications to monadic decomposition)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Latticed \(k\)-induction with an application to probabilistic programs
- Lower-bound synthesis using loop specialization and Max-SMT
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Runtime monitors for Markov decision processes
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Coming to terms with quantified reasoning
- Automated inference of gene regulatory networks using explicit regulatory modules
- EUFORIA: complete software model checking with uninterpreted functions
- Optimized temporal monitors for SystemcC
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Automatic generation of logical models with AGES
- Automatic discovery of fair paths in infinite-state transition systems
- Learning linear temporal properties from noisy data: a MaxSAT-based approach
- Symbolic computation of differential equivalences
- Constraint programming for dynamic symbolic execution of JavaScript
- Probabilistic software product lines
- On the initialization of clocks in timed formalisms
- Computational verification of network programs in Coq
- Software model checking
- Scalable fine-grained proofs for formula processing
- A neurally-guided, parallel theorem prover
- Admissibility in Probabilistic Argumentation
- Assume, guarantee or repair
- Skill-based verification of cyber-physical systems
- Virtual substitution for SMT-solving
- Reachability in timed automata with diagonal constraints
- A framework for model transformation verification
- ProofWidgets
- Being careful about theory combination
This page was built for software: z3
