Superposition as a decision procedure for timed automata
type: Item
instance of: scholarly article
title: Superposition as a decision procedure for timed automata
zbMATH Open document ID: 1262.68159
author: Arnaud Fietzke
author: Christoph Weidenbach
published in: Mathematics in Computer Science
publication date: 2013-04-25T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 6157645
zbMATH Keywords: superposition
zbMATH Keywords: hierarchic theorem proving
zbMATH Keywords: timed automata
zbMATH Keywords: decision procedures
describes a project that uses: Uppaal
describes a project that uses: Kronos
describes a project that uses: YAGO
MaRDI profile type: Publication
full work available at URL: s11786-012-0134-5
OpenAlex ID: W2076908710
cites work: Superposition Modulo Linear Arithmetic SUP(LA)
cites work: Q4036557
cites work: Model-checking in dense real-time
cites work: A theory of timed automata
cites work: New results on rewrite-based satisfiability procedures
cites work: Q4785507
cites work: Q4422082
cites work: Resolution theorem proving
cites work: Q4282593
cites work: Refutational theorem proving for hierarchic first-order theories
cites work: (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
cites work: Automated Deduction – CADE-20
cites work: Formal Methods for the Design of Real-Time Systems
cites work: Lectures on Concurrency and Petri Nets
cites work: On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
cites work: Formal Modeling and Analysis of Timed Systems
cites work: Q4809077
cites work: Engineering DPLL(T) + Saturation
cites work: Resolution decision procedures
cites work: Superposition-Based Analysis of First-Order Probabilistic Timed Automata
cites work: Automatic Generation of Invariants for Circular Derivations in SUP(LA)
cites work: Q2723913
cites work: Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
cites work: Presburger arithmetic with unary predicates is Π11 complete
cites work: Symbolic model checking for real-time systems
cites work: Superposition for Fixed Domains
cites work: Q3838762
cites work: Integrating Linear Arithmetic into Superposition Calculus
cites work: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
cites work: Uppaal in a nutshell
cites work: Q5590814
cites work: Solving SAT and SAT Modulo Theories
cites work: Paramodulation-based theorem proving
cites work: Q4953405
cites work: Q4818802
cites work: A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
cites work: Bounded model checking for timed automata
cites work: On the Saturation of YAGO
cites work: Q5792485
cites work: Q4539608
cites work: Kronos: A verification tool for real-time systems
DOI: 10.1007/S11786-012-0134-5
description: scientific article; zbMATH DE number 6157645