The following pages link to z3 (Q17039):
Displaying 50 items.
- Combined task- and network-level scheduling for distributed time-triggered systems (Q258438) (← links)
- A tool for deciding the satisfiability of continuous-time metric temporal logic (Q262137) (← links)
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- Deciding probabilistic automata weak bisimulation: theory and practice (Q282105) (← links)
- Proof tree preserving tree interpolation (Q286737) (← links)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- MizAR 40 for Mizar 40 (Q286800) (← links)
- Decision procedures for flat array properties (Q287272) (← links)
- Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
- An experiment with satisfiability modulo SAT (Q287334) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A heuristic prover for real inequalities (Q287379) (← links)
- Adding decision procedures to SMT solvers using axioms with triggers (Q287384) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- LCTD: test-guided proofs for C programs on LLVM (Q338629) (← links)
- Detection of Hopf bifurcations in chemical reaction networks using convex coordinates (Q349840) (← links)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Simulating circuit-level simplifications on CNF (Q352967) (← links)
- Minimal counterexamples for linear-time probabilistic verification (Q402125) (← links)
- Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26--29, 2012. Proceedings (Q428512) (← links)
- Combining decision procedures by (model-)equality propagation (Q436376) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- SAT modulo linear arithmetic for solving polynomial constraints (Q438576) (← links)
- An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers (Q453505) (← links)
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (Q457250) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- Constraint LTL satisfiability checking without automata (Q472802) (← links)
- SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (Q479819) (← links)
- An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
- Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
- Verifying global start-up for a Möbius ring-oscillator (Q479839) (← links)
- Solving constraint satisfaction problems with SAT modulo theories (Q487632) (← links)
- A calculus of quality for robustness against unreliable communication (Q492911) (← links)
- Parametrized invariance for infinite state processes (Q493122) (← links)
- Program equivalence by circular reasoning (Q493521) (← links)
- Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers (Q497870) (← links)
- Complexity of fixed-size bit-vector logics (Q504997) (← links)
- A generic framework for symbolic execution: a coinductive approach (Q507361) (← links)
- Empirical decision model learning (Q511793) (← links)
- SMT-based model checking for recursive programs (Q518396) (← links)
- An efficient SMT solver for string constraints (Q518402) (← links)
- From invariant checking to invariant inference using randomized search (Q518404) (← links)
- A search-based procedure for nonlinear real arithmetic (Q518407) (← links)
- Decision procedures. An algorithmic point of view (Q518892) (← links)
- Z3str2: an efficient solver for strings, regular expressions, and length constraints (Q526767) (← links)
- Automated deduction -- CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 -- August 5, 2011. Proceedings (Q555523) (← links)
- Effective abstractions for verification under relaxed memory models (Q681346) (← links)
- Composing model programs for analysis (Q710670) (← links)
