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
• LCF-style bit-blasting in HOL4
• 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
• Lazy synthesis
• A new probabilistic constraint logic programming language based on a generalised distribution semantics
• 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
• 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
• A practical approach to model checking duration calculus using Presburger arithmetic
• Modeling high school timetabling with bitvectors
• Minimal counterexamples for linear-time probabilistic verification
• Optimized temporal monitors for SystemcC
• Multi-dimensional interpretations for termination of term rewriting
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• An Evaluation of Automata Algorithms for String Analysis
• Error Invariants
• Separation logics and modalities: a survey
• Chain-Free String Constraints
• Title not available (Why is that?)
• Automating Inductive Proofs Using Theory Exploration
• Functional Analysis of Large-Scale DNA Strand Displacement Circuits
• Combining Decision Procedures by (Model-)Equality Propagation
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Real World Verification
• Compositional may-must program analysis
• A Basis for Verifying Multi-threaded Programs
• Quantifier-free interpolation in combinations of equality interpolating theories
• Combining decision procedures by (model-)equality propagation
• An instantiation scheme for satisfiability modulo theories
• SAT modulo linear arithmetic for solving polynomial constraints
• The complexity of reversal-bounded model-checking
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• On deciding satisfiability by theorem proving with speculative inferences
• An extension of lazy abstraction with interpolation for programs with arrays
• Deciding floating-point logic with abstract conflict driven clause learning
• Fast LCF-Style Proof Reconstruction for Z3
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26--29, 2012. Proceedings
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS

This page was built for software: z3