z3

swMATH4887MaRDI QIDQ17039FDOQ17039

Author name not available (Why is that?)

Source code repository: https://github.com/Z3Prover/z3

Cited In (only showing first 100 items - show all)

• Symbolic computation of differential equivalences
• Scalable fine-grained proofs for formula processing
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• Optimization modulo non-linear arithmetic via incremental linearization
• 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
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
• Automatically disproving fair termination of higher-order functional programs
• Algorithmic reduction of biological networks with multiple time scales
• Reliable reconstruction of fine-grained proofs in a proof assistant
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• An SMT theory of fixed-point arithmetic
• Integrating Simplex with Tableaux
• On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
• Runtime complexity analysis of logically constrained rewriting
• On the complexity of reconstructing chemical reaction networks
• Refutation-based synthesis in SMT
• Optimization modulo the theory of floating-point numbers
• SPASS-SATT. A CDCL(LA) solver
• Towards more efficient methods for solving regular-expression heavy string constraints
• Automated verification of practical garbage collectors
• Deciding Bit-Vector Formulas with mcSAT
• Lower Runtime Bounds for Integer Programs
• A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
• Automatic Generation of Invariants for Circular Derivations in SUP(LA)
• An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
• Solving Nonlinear Integer Arithmetic with MCSAT
• A new probabilistic constraint logic programming language based on a generalised distribution semantics
• LCF-Style Bit-Blasting in HOL4
• Certified Roundoff Error Bounds Using Semidefinite Programming
• Bounded Quantifier Instantiation for Checking Inductive Invariants
• Congruence Closure with Free Variables
• Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
• Probabilistic satisfiability: algorithms with the presence and absence of a phase transition
• Exploring Theories with a Model-Finding Assistant
• Analysis of Reaction Network Systems Using Tropical Geometry
• Extensional Crisis and Proving Identity
• Chemical reaction networks and stochastic local search
• Matching Logic
• Lazy Synthesis
• Improving the numerical stability of fast matrix multiplication
• Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
• A Calculus for Modular Loop Acceleration
• Structural Reductions Revisited
• Local algebraic effect theories
• Title not available (Why is that?)
• Caper
• Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing
• Verifying Procedural Programs via Constrained Rewriting Induction
• A constraint-based approach to solving games on infinite graphs
• Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
• Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
• Fast Cube Tests for LIA Constraint Solving
• Formal Mathematics on Display: A Wiki for Flyspeck
• Coming to terms with quantified reasoning
• Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions
• What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
• Satisfiability Checking: Theory and Applications
• Model Finding for Recursive Functions in SMT
• Term orderings for non-reachability of (conditional) rewriting
• Automated Discovery of Simulation Between Programs
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Towards Quantitative Verification of Reaction Systems
• Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• A set solver for finite set relation algebra
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• Volume Computation for Boolean Combination of Linear Arithmetic Constraints
• Automated Improving of Proof Legibility in the Mizar System
• Fields of logic and computation. Essays dedicated to Yuri Gurevich on the occasion of his 70th birthday
• Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
• Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
• A non-linear arithmetic procedure for control-command software verification
• Secure Guarded Commands
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• Instrumenting a weakest precondition calculus for counterexample generation
• Formal verification of masked hardware implementations in the presence of glitches
• Satisfiability modulo theory (SMT) formulation for optimal scheduling of task graphs with communication delay
• Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
• Subsumption demodulation in first-order theorem proving
• Computing and estimating the volume of the solution space of SMT(LA) constraints

This page was built for software: z3