Sciweavers

CAV
2012
Springer
334views Hardware» more  CAV 2012»
12 years 1 months ago
Joogie: Infeasible Code Detection for Java
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...
Stephan Arlt, Martin Schäf
CAV
2012
Springer
241views Hardware» more  CAV 2012»
12 years 1 months ago
Bma: Visual Tool for Modeling and Analyzing Biological Networks
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...
David Benque, Sam Bourton, Caitlin Cockerton, Byro...
CAV
2012
Springer
270views Hardware» more  CAV 2012»
12 years 1 months ago
Automated Termination Proofs for Java Programs with Cyclic Data
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...
Marc Brockschmidt, Richard Musiol, Carsten Otto, J...
CAV
2012
Springer
265views Hardware» more  CAV 2012»
12 years 1 months ago
An Axiomatic Memory Model for POWER Multiprocessors
The growing complexity of hardware optimizations employed by multiprocessors leads to subtle distinctions among allowed and disallowed behaviors, posing challenges in specifying th...
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayv...
CAV
2012
Springer
222views Hardware» more  CAV 2012»
12 years 1 months ago
Leveraging Interpolant Strength in Model Checking
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...
Simone Fulvio Rollini, Ondrej Sery, Natasha Sharyg...