An interpolating decision procedure for transitive relations with uninterpreted functions

An interpolating decision procedure for transitive relations with uninterpreted functions

अन्य संस्करण दिखाएं (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...

पूर्ण विवरण

ग्रंथसूची विवरण
मुख्य लेखकों:	Kroening, D, Weissenbacher, G
अन्य लेखक:	Namjoshi, K
स्वरूप:	Book section
भाषा:	English
प्रकाशित:	2009
विषय:	Theory and automated verification Computer science (mathematics)

समान संसाधन

An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
द्वारा: Kroening, D, और अन्य
प्रकाशित: (2010)

Program analysis with interpolants
द्वारा: Weissenbacher, G, और अन्य
प्रकाशित: (2010)

Repairing strings and trees
द्वारा: Riveros Jaeger, C
प्रकाशित: (2013)

Abstract satisfaction
द्वारा: Haller, L
प्रकाशित: (2013)

EL-ifying ontologies
द्वारा: Carral, D, और अन्य
प्रकाशित: (2014)

Pushing the boundaries of tractable ontology reasoning
द्वारा: Carral, D, और अन्य
प्रकाशित: (2014)

Synthesis and alternating automata over real time
द्वारा: Jenkins, M, और अन्य
प्रकाशित: (2012)

Static analyses over weak memory
द्वारा: Nimal, V, और अन्य
प्रकाशित: (2014)

Verification of asynchronous concurrency and the shaped stack constraint
द्वारा: Kochems, J
प्रकाशित: (2014)

Higher-order semantics for quantum programming languages with classical control
द्वारा: Atzemoglou, GP
प्रकाशित: (2012)

Formal methods for the analysis of wireless network protocols
द्वारा: Fruth, M
प्रकाशित: (2011)

Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
द्वारा: Adams, S
प्रकाशित: (2014)

A hierarchy of failures-based models: theory and application
द्वारा: Bolton, C, और अन्य
प्रकाशित: (2005)

Topics in monitoring and planning for embedded real-time systems
द्वारा: Ho, H
प्रकाशित: (2015)

Saturation methods for global model-checking pushdown systems
द्वारा: Hague, M
प्रकाशित: (2009)

Pictures of processes
द्वारा: Kissinger, A
प्रकाशित: (2011)

Program synthesis from domain specific object models
द्वारा: Faitelson, D
प्रकाशित: (2008)

Monotonicity in shared-memory program verification
द्वारा: Kaiser, A
प्रकाशित: (2013)

Automated quantitative software verification
द्वारा: Kattenbelt, M
प्रकाशित: (2010)

Forward looking logics and automata
द्वारा: Ley, C
प्रकाशित: (2011)

Intersection types and higer-order model checking
द्वारा: Ramsay, S, और अन्य
प्रकाशित: (2014)

Precise verification of C programs
द्वारा: Lewis, M
प्रकाशित: (2014)

Probabilistic guarded commands mechanized in HOL
द्वारा: Hurd, J, और अन्य
प्रकाशित: (2005)

Incremental modelling for verified communication architectures
द्वारा: Boehm, P, और अन्य
प्रकाशित: (2011)

Functions with local state: regularity and undecidability
द्वारा: Murawski, A
प्रकाशित: (2005)

On learning assumptions for compositional verification of probabilistic systems
द्वारा: Feng, L
प्रकाशित: (2014)

Quantitative verification of real-time properties with application to medical devices
द्वारा: Marco Diciolla, M, और अन्य
प्रकाशित: (2014)

Reasoning with !-graphs
द्वारा: Merry, A
प्रकाशित: (2013)

Non-Philosophy and the uninterpretable axiom
द्वारा: Ameen Mettawa
प्रकाशित: (2018-09-01)

Non-Philosophy and the uninterpretable axiom
द्वारा: Ameen Mettawa
प्रकाशित: (2018-09-01)

Game semantics based equivalence checking of higher-order programs
द्वारा: Hopkins, D, और अन्य
प्रकाशित: (2012)

Instantiating uninterpreted functional units and memory system: functional verification of the VAMP processor
द्वारा: Beyer, S, और अन्य
प्रकाशित: (2003)

Predicate Abstraction of ANSI-C Programs Using SAT
द्वारा: Clarke, E, और अन्य
प्रकाशित: (2004)

An algebraic theory of componentised interaction
द्वारा: Chilton, C
प्रकाशित: (2013)

Tractable query answering for description logics via query rewriting
द्वारा: Perez-Urbina, H, और अन्य
प्रकाशित: (2010)

The formal semantics of a domain-specific modelling language
द्वारा: Grealish, C
प्रकाशित: (2010)

Partial correctness for probabilistic demonic programs
द्वारा: McIver, A, और अन्य
प्रकाशित: (2001)

Model Checking Systems with Replicated Components using CSP
द्वारा: Mazur, T
प्रकाशित: (2011)

Central limit model checking
द्वारा: Bortolussi, L, और अन्य
प्रकाशित: (2018)

Interpolant-Based Transition Relation Approximation
द्वारा: Ranjit Jhala, और अन्य
प्रकाशित: (2007-11-01)