Superposition as a decision procedure for timed automata (Q1949086): Difference between revisions

@@ Property / cites work @@
+Superposition Modulo Linear Arithmetic SUP(LA)
@@ Property / cites work: Superposition Modulo Linear Arithmetic SUP(LA) / rank @@
+Normal rank
@@ Property / cites work @@
+Q4036557
@@ Property / cites work: Q4036557 / rank @@
+Normal rank
@@ Property / cites work @@
+Model-checking in dense real-time
@@ Property / cites work: Model-checking in dense real-time / rank @@
+Normal rank
@@ Property / cites work @@
+A theory of timed automata
@@ Property / cites work: A theory of timed automata / rank @@
+Normal rank
@@ Property / cites work @@
+New results on rewrite-based satisfiability procedures
+Normal rank
@@ Property / cites work @@
+Q4785507
@@ Property / cites work: Q4785507 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4422082
@@ Property / cites work: Q4422082 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4282593
@@ Property / cites work: Q4282593 / rank @@
+Normal rank
@@ Property / cites work @@
+Refutational theorem proving for hierarchic first-order theories
+Normal rank
@@ Property / cites work @@
+(LIA) - Model Evolution with Linear Integer Arithmetic Constraints
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Methods for the Design of Real-Time Systems
+Normal rank
@@ Property / cites work @@
+Lectures on Concurrency and Petri Nets
@@ Property / cites work: Lectures on Concurrency and Petri Nets / rank @@
+Normal rank
@@ Property / cites work @@
+On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
+Normal rank
@@ Property / cites work @@
+Formal Modeling and Analysis of Timed Systems
@@ Property / cites work: Formal Modeling and Analysis of Timed Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809077
@@ Property / cites work: Q4809077 / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering DPLL(T) + Saturation
@@ Property / cites work: Engineering DPLL(T) + Saturation / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751377
@@ Property / cites work: Q2751377 / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition-Based Analysis of First-Order Probabilistic Timed Automata
+Normal rank
@@ Property / cites work @@
+Automatic Generation of Invariants for Circular Derivations in SUP(LA)
+Normal rank
@@ Property / cites work @@
+Q2723913
@@ Property / cites work: Q2723913 / rank @@
+Normal rank
@@ Property / cites work @@
+Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
+Normal rank
@@ Property / cites work @@
+Presburger arithmetic with unary predicates is <i>Π</i><sub>1</sub><sup>1</sup> complete
+Normal rank
@@ Property / cites work @@
+Symbolic model checking for real-time systems
@@ Property / cites work: Symbolic model checking for real-time systems / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition for Fixed Domains
@@ Property / cites work: Superposition for Fixed Domains / rank @@
+Normal rank
@@ Property / cites work @@
+Q3838762
@@ Property / cites work: Q3838762 / rank @@
+Normal rank
@@ Property / cites work @@
+Integrating Linear Arithmetic into Superposition Calculus
+Normal rank
@@ Property / cites work @@
+Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
+Normal rank
@@ Property / cites work @@
+Uppaal in a nutshell
@@ Property / cites work: Uppaal in a nutshell / rank @@
+Normal rank
@@ Property / cites work @@
+Q5590814
@@ Property / cites work: Q5590814 / rank @@
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751359
@@ Property / cites work: Q2751359 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4953405
@@ Property / cites work: Q4953405 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4818802
@@ Property / cites work: Q4818802 / rank @@
+Normal rank
@@ Property / cites work @@
+A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
+Normal rank
@@ Property / cites work @@
+Q2842869
@@ Property / cites work: Q2842869 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Saturation of YAGO
@@ Property / cites work: On the Saturation of YAGO / rank @@
+Normal rank
@@ Property / cites work @@
+Q5792485
@@ Property / cites work: Q5792485 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4539608
@@ Property / cites work: Q4539608 / rank @@
+Normal rank
@@ Property / cites work @@
+Kronos: A verification tool for real-time systems
@@ Property / cites work: Kronos: A verification tool for real-time systems / rank @@
+Normal rank