An interpolating decision procedure for transitive relations with uninterpreted functions

An interpolating decision procedure for transitive relations with uninterpreted functions

Taispeáin leaganacha eile (1)

We present a proof-generating decision procedure for the quantifier-free fragment of first-order logic with the relations =, !=, >=, and > and argue that this logic, augmented with a set of theory-specific rewriting rules, is adequate for bit-level accurate verification. We describe ou...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Kroening, D, Weissenbacher, G
Rannpháirtithe:	Namjoshi, K
Formáid:	Book section
Teanga:	English
Foilsithe / Cruthaithe:	2009
Ábhair:	Theory and automated verification Computer science (mathematics)

Míreanna comhchosúla

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2010)

Program analysis with interpolants
de réir: Weissenbacher, G, et al.
Foilsithe / Cruthaithe: (2010)

Repairing strings and trees
de réir: Riveros Jaeger, C
Foilsithe / Cruthaithe: (2013)

Abstract satisfaction
de réir: Haller, L
Foilsithe / Cruthaithe: (2013)

EL-ifying ontologies
de réir: Carral, D, et al.
Foilsithe / Cruthaithe: (2014)

Pushing the boundaries of tractable ontology reasoning
de réir: Carral, D, et al.
Foilsithe / Cruthaithe: (2014)

Synthesis and alternating automata over real time
de réir: Jenkins, M, et al.
Foilsithe / Cruthaithe: (2012)

Static analyses over weak memory
de réir: Nimal, V, et al.
Foilsithe / Cruthaithe: (2014)

Verification of asynchronous concurrency and the shaped stack constraint
de réir: Kochems, J
Foilsithe / Cruthaithe: (2014)

Higher-order semantics for quantum programming languages with classical control
de réir: Atzemoglou, GP
Foilsithe / Cruthaithe: (2012)

Formal methods for the analysis of wireless network protocols
de réir: Fruth, M
Foilsithe / Cruthaithe: (2011)

Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
de réir: Adams, S
Foilsithe / Cruthaithe: (2014)

A hierarchy of failures-based models: theory and application
de réir: Bolton, C, et al.
Foilsithe / Cruthaithe: (2005)

Topics in monitoring and planning for embedded real-time systems
de réir: Ho, H
Foilsithe / Cruthaithe: (2015)

Saturation methods for global model-checking pushdown systems
de réir: Hague, M
Foilsithe / Cruthaithe: (2009)

Pictures of processes
de réir: Kissinger, A
Foilsithe / Cruthaithe: (2011)

Program synthesis from domain specific object models
de réir: Faitelson, D
Foilsithe / Cruthaithe: (2008)

Monotonicity in shared-memory program verification
de réir: Kaiser, A
Foilsithe / Cruthaithe: (2013)

Automated quantitative software verification
de réir: Kattenbelt, M
Foilsithe / Cruthaithe: (2010)

Forward looking logics and automata
de réir: Ley, C
Foilsithe / Cruthaithe: (2011)

Intersection types and higer-order model checking
de réir: Ramsay, S, et al.
Foilsithe / Cruthaithe: (2014)

Precise verification of C programs
de réir: Lewis, M
Foilsithe / Cruthaithe: (2014)

Probabilistic guarded commands mechanized in HOL
de réir: Hurd, J, et al.
Foilsithe / Cruthaithe: (2005)

Incremental modelling for verified communication architectures
de réir: Boehm, P, et al.
Foilsithe / Cruthaithe: (2011)

Functions with local state: regularity and undecidability
de réir: Murawski, A
Foilsithe / Cruthaithe: (2005)

On learning assumptions for compositional verification of probabilistic systems
de réir: Feng, L
Foilsithe / Cruthaithe: (2014)

Quantitative verification of real-time properties with application to medical devices
de réir: Marco Diciolla, M, et al.
Foilsithe / Cruthaithe: (2014)

Reasoning with !-graphs
de réir: Merry, A
Foilsithe / Cruthaithe: (2013)

Non-Philosophy and the uninterpretable axiom
de réir: Ameen Mettawa
Foilsithe / Cruthaithe: (2018-09-01)

Non-Philosophy and the uninterpretable axiom
de réir: Ameen Mettawa
Foilsithe / Cruthaithe: (2018-09-01)

Game semantics based equivalence checking of higher-order programs
de réir: Hopkins, D, et al.
Foilsithe / Cruthaithe: (2012)

Instantiating uninterpreted functional units and memory system: functional verification of the VAMP processor
de réir: Beyer, S, et al.
Foilsithe / Cruthaithe: (2003)

Predicate Abstraction of ANSI-C Programs Using SAT
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

An algebraic theory of componentised interaction
de réir: Chilton, C
Foilsithe / Cruthaithe: (2013)

Tractable query answering for description logics via query rewriting
de réir: Perez-Urbina, H, et al.
Foilsithe / Cruthaithe: (2010)

The formal semantics of a domain-specific modelling language
de réir: Grealish, C
Foilsithe / Cruthaithe: (2010)

Partial correctness for probabilistic demonic programs
de réir: McIver, A, et al.
Foilsithe / Cruthaithe: (2001)

Model Checking Systems with Replicated Components using CSP
de réir: Mazur, T
Foilsithe / Cruthaithe: (2011)

Central limit model checking
de réir: Bortolussi, L, et al.
Foilsithe / Cruthaithe: (2018)

Interpolant-Based Transition Relation Approximation
de réir: Ranjit Jhala, et al.
Foilsithe / Cruthaithe: (2007-11-01)