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
• Secure guarded commands
• Modular verification of procedure equivalence in the presence of memory allocation
• Formal verification of a C-like memory model and its uses for verifying program transformations
• LCF-style bit-blasting in HOL4
• Automatically disproving fair termination of higher-order functional programs
• Analysis of reaction network systems using tropical geometry
• Exploring theories with a model-finding assistant
• Extensional crisis and proving identity
• Polyhedral approximation of multivariate polynomials using Handelman's theorem
• Lower runtime bounds for integer programs
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• Solving nonlinear integer arithmetic with MCSAT
• Verifying procedural programs via constrained rewriting induction
• Certified roundoff error bounds using semidefinite programming
• Matching logic
• Bounded quantifier instantiation for checking inductive invariants
• Arrays made simpler: an efficient, scalable and thorough preprocessing
• Incomplete SMT techniques for solving non-linear formulas over the integers
• Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
• Congruence closure with free variables
• Structural reductions revisited
• A calculus for modular loop acceleration
• Reliable reconstruction of fine-grained proofs in a proof assistant
• An SMT theory of fixed-point arithmetic
• 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
• Automatic Generation of Invariants for Circular Derivations in SUP(LA)
• An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
• Lazy synthesis
• A new probabilistic constraint logic programming language based on a generalised distribution semantics
• Probabilistic satisfiability: algorithms with the presence and absence of a phase transition
• Chemical reaction networks and stochastic local search
• Improving the numerical stability of fast matrix multiplication
• Local algebraic effect theories
• Title not available (Why is that?)
• Caper
• A constraint-based approach to solving games on infinite graphs
• Integrating simplex with tableaux
• Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• Extending Sledgehammer with SMT solvers
• CompoSAT: specification-guided coverage for model finding
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Combined task- and network-level scheduling for distributed time-triggered systems
• MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions
• Regression verification for unbalanced recursive functions
• Automated inference of gene regulatory networks using explicit regulatory modules
• EUFORIA: complete software model checking with uninterpreted functions
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• Automatic generation of logical models with AGES
• Symbolic abstract contract synthesis in a rewriting framework
• A self-certifying compilation framework for WebAssembly
• Constraint LTL satisfiability checking without automata
• Wombit: a portfolio bit-vector solver using word-level propagation
• Automating Induction with an SMT Solver
• Contract-based verification of MATLAB-style matrix programs
• Deciding probabilistic automata weak bisimulation: theory and practice
• An SMT-based approach to satisfiability checking of MITL
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• From invariant checking to invariant inference using randomized search
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Proof tree preserving tree interpolation
• Decision procedures for flat array properties
• Interpolation systems for ground proofs in automated deduction: a survey
• An experiment with satisfiability modulo SAT
• A heuristic prover for real inequalities
• Adding decision procedures to SMT solvers using axioms with triggers
• Semi-intelligible Isar proofs from machine-generated proofs

This page was built for software: z3