Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CAV
2012
Springer
222views Hardware» more  CAV 2012»
9 years 4 months ago
OpenNWA: A Nested-Word Automaton Library
Nested-word automata (NWAs) are a language formalism that helps bridge the gap between finite-state automata and pushdown automata. NWAs can express some context-free properties, ...
Evan Driscoll, Aditya V. Thakur, Thomas W. Reps
CAV
2012
Springer
227views Hardware» more  CAV 2012»
9 years 4 months ago
Minimum Satisfying Assignments for SMT
Abstract. A minimum satisfying assignment of a formula is a minimumcost partial assignment of values to the variables in the formula that guarantees the formula is true. Minimum sa...
Isil Dillig, Thomas Dillig, Kenneth L. McMillan, A...
CAV
2012
Springer
223views Hardware» more  CAV 2012»
9 years 4 months ago
Detecting Fair Non-termination in Multithreaded Programs
Abstract. We develop compositional analysis algorithms for detecting nontermination in multithreaded programs. Our analysis explores fair and ultimatelyperiodic executions—i.e., ...
Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi...
CAV
2012
Springer
236views Hardware» more  CAV 2012»
9 years 4 months ago
Lock Removal for Concurrent Trace Programs
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...
Vineet Kahlon, Chao Wang
CAV
2012
Springer
231views Hardware» more  CAV 2012»
9 years 4 months ago
Incremental, Inductive CTL Model Checking
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...
Zyad Hassan, Aaron R. Bradley, Fabio Somenzi
CAV
2012
Springer
198views Hardware» more  CAV 2012»
9 years 4 months ago
Termination Analysis with Algorithmic Learning
An algorithmic-learning-based termination analysis technique is presented. The new technique combines transition predicate abstraction, algorithmic learning, and decision procedure...
Wonchan Lee, Bow-Yaw Wang, Kwangkeun Yi
CAV
2012
Springer
257views Hardware» more  CAV 2012»
9 years 4 months ago
CSolve: Verifying C with Liquid Types
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...
Patrick Maxim Rondon, Alexander Bakst, Ming Kawagu...
CAV
2012
Springer
242views Hardware» more  CAV 2012»
9 years 4 months ago
Exercises in Nonstandard Static Analysis of Hybrid Systems
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...
Ichiro Hasuo, Kohei Suenaga
CAV
2012
Springer
251views Hardware» more  CAV 2012»
9 years 4 months ago
A Model Checker for Hierarchical Probabilistic Real-Time Systems
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...
Songzheng Song, Jun Sun 0001, Yang Liu 0003, Jin S...
CAV
2012
Springer
243views Hardware» more  CAV 2012»
9 years 4 months ago
SPT: Storyboard Programming Tool
elor Thesis: Demand Driven Abstraction Refinement Kendriya Vidyalaya ONGC, Dehradun, Uttaranchal INDIA All India Senior Secondary Examination, May 2004 • Secured 97.6 % marks in...
Rishabh Singh, Armando Solar-Lezama
books