CAV
2012
Springer
12 years 2 months ago
2012
Springer
Abstract. We develop compositional analysis algorithms for detecting nontermination in multithreaded programs. Our analysis explores fair and ultimatelyperiodic executions—i.e., ...
CAV
2012
Springer
12 years 2 months ago
2012
Springer
Abstract. We propose a trace-based concurrent program analysis to soundly remove redundant synchronizations such as locks while preserving the behaviors of the concurrent computati...
CAV
2012
Springer
12 years 2 months ago
2012
Springer
A SAT-based incremental, inductive algorithm for model checking CTL properties is proposed. As in classic CTL model checking, the parse graph of the property shapes the analysis. H...
CAV
2012
Springer
12 years 2 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...
CAV
2012
Springer
12 years 2 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...
CAV
2012
Springer
12 years 2 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...
CAV
2012
Springer
12 years 2 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...
CAV
2012
Springer
12 years 2 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...
CAV
2012
Springer
12 years 2 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...
CAV
2012
Springer
12 years 2 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...