145
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
An algorithmic-learning-based termination analysis technique is presented. The new technique combines transition predicate abstraction, algorithmic learning, and decision procedure...
145
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
We present CSolve, an automated verifier for C programs based on Liquid Type inference. We show how CSolve verifies memory safety through an example and describe its architecture...
152
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
Abstract. In formal verification of hybrid systems, a big challenge is to incorporate continuous flow dynamics in a discrete framework. Our previous work proposed to use nonstand...
167
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
Real-life systems are usually hard to control, due to their complicated structures, quantitative time factors and even stochastic behaviors. In this work, we present a model checke...
130
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
elor Thesis: Demand Driven Abstraction Refinement Kendriya Vidyalaya ONGC, Dehradun, Uttaranchal INDIA All India Senior Secondary Examination, May 2004 • Secured 97.6 % marks in...
205
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
We present Joogie, a tool that detects infeasible code in Java programs. Infeasible code is code that does not occur on feasible controlflow paths and thus has no feasible executi...
235
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
Abstract. BioModel Analyzer (bma) is a tool for modeling and analyzing biological networks. Designed with a lightweight graphical user interface, the tool facilitates usage for bio...
163
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
Abstract. In earlier work, we developed a technique to prove termination of Java programs automatically: first, Java programs are automatically transformed to term rewrite systems...
119
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
The growing complexity of hardware optimizations employed by multiprocessors leads to subtle distinctions among allowed and disallowed behaviors, posing challenges in specifying th...
161
click to vote
CAV
2012
Springer
13 years 7 months ago
2012
Springer
Craig interpolation is a well known method of abstraction successfully used in both hardware and software model checking. The logical strength of interpolants can affect the quali...