Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
VSTTE
2012
Springer
8 years 8 months ago
Deciding Functional Lists with Sublist Sets
Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functio...
Thomas Wies, Marco Muñiz, Viktor Kuncak
VLC
2011
83views more  VLC 2011»
9 years 8 months ago
A decision procedure for a decidable fragment of generalized constraint diagrams
Constraint diagrams were introduced by Kent, in 1997, as an alternative to the OCL for placing formal constraints on software models. Since their introduction, constraint diagrams...
Jim Burton, Gem Stapleton, Ali Hamie
LICS
2010
IEEE
9 years 11 months ago
Regular Cost Functions over Finite Trees
We develop the theory of regular cost functions over finite trees: a quantitative extension to the notion of regular languages of trees: Cost functions map each input (tree) to a v...
Thomas Colcombet, Christof Löding
CADE
2010
Springer
9 years 11 months ago
Terminating Tableaux for Hybrid Logic with Eventualities
x-free and employs a novel clausal form that abstracts away from propositional reasoning. It comes with an elegant correctness proof. We discuss some optimizations for decision pro...
Mark Kaminski, Gert Smolka
JSC
2010
120views more  JSC 2010»
9 years 11 months ago
Theory decision by decomposition
The topic of this article is decision procedures for satisfiability modulo theories (SMT) of arbitrary quantifier-free formulæ. We propose an approach that decomposes the formu...
Maria Paola Bonacina, Mnacho Echenim
JANCL
2006
105views more  JANCL 2006»
10 years 1 months ago
BDD-based decision procedures for the modal logic K
We describe BDD-based decision procedures for the modal logic K. Our approach is inspired by the automata-theoretic approach, but we avoid explicit automata construction. Instead, ...
Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi
IPL
2006
109views more  IPL 2006»
10 years 1 months ago
Knuth-Bendix completion of theories of commuting group endomorphisms
Knuth-Bendix completions of the equational theories of k 2 commuting group endomorphisms are obtained, using automated theorem proving and modern termination checking. This impro...
Aaron Stump, Bernd Löchner
IANDC
2006
79views more  IANDC 2006»
10 years 1 months ago
Efficient theory combination via boolean search
Many approaches to deciding the satisfiability of quantifier free formulae with respect to a background theory T -- also known as Satisfiability Modulo Theory, or SMT
Marco Bozzano, Roberto Bruttomesso, Alessandro Cim...
ENTCS
2006
125views more  ENTCS 2006»
10 years 1 months ago
An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving
To broaden the scope of decision procedures for linear arithmetic, they have to be integrated into theorem provers. Successful approaches e.g. in NQTHM or ACL2 suggest a close int...
Tobias Schmidt-Samoa
APLAS
2010
ACM
10 years 1 months ago
Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates
Abstract. By combining algorithmic learning, decision procedures, predicate abstraction, and simple templates, we present an automated technique for finding quantified loop invaria...
Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw...
books