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)