156
click to vote
CADE
2012
Springer
13 years 6 months ago
2012
Springer
We propose a word level, bounded model checking (BMC) algorithm based on translation into the effectively propositional fragment (EPR) of firstorder logic. This approach to BMC al...
136
click to vote
CADE
2012
Springer
13 years 6 months ago
2012
Springer
We introduce a technique to prove non-termination of term rewrite systems automatically. Our technique improves over previous approaches substantially, as it can also detect non-lo...
152
click to vote
CADE
2012
Springer
13 years 6 months ago
2012
Springer
Abstract. This paper presents new results on the decidability of inductive validity of conjectures. For these results, a class of term rewrite systems (TRSs) with built-in linear i...
153
click to vote
CADE
2012
Springer
13 years 6 months ago
2012
Springer
The problem of SPARQL query containment is defined as determining if the result of one query is included in the result of another for any RDF graph. Query containment is important...
152
click to vote
CADE
2012
Springer
13 years 6 months ago
2012
Springer
Abstract. Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known c...
181
click to vote
CADE
2012
Springer
13 years 6 months ago
2012
Springer
Abstract. This paper describes a novel decision procedure for quantifierfree linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domai...
310
click to vote
ICFP
2012
ACM
13 years 6 months ago
2012
ACM
Graphics processing units (GPUs) provide both memory bandwidth and arithmetic performance far greater than that available on CPUs but, because of their Single-Instruction-Multiple...
186
click to vote
ICFP
2012
ACM
13 years 6 months ago
2012
ACM
In the static analysis of functional programs, pushdown flow analabstract garbage collection skirt just inside the boundaries of soundness and decidability. Alone, each method re...
165
click to vote
ICFP
2012
ACM
13 years 6 months ago
2012
ACM
Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: we can finally write correct-by-cons...
169
click to vote
ICFP
2012
ACM
13 years 6 months ago
2012
ACM
The higher-order logic found in proof assistants such as Coq and various HOL systems provides a convenient setting for the development and verification of pure functional program...