CAV
2011
Springer
12 years 8 months ago
2011
Springer
Abstract. We present a novel static analysis technique that substantially improves the quality of invariants inferred by standard loop invariant generation techniques. Our techniqu...
CAV
2011
Springer
12 years 8 months ago
2011
Springer
We updated our Peggy tool, previously presented in [6], to perform translation validation for the LLVM compiler using a technique called Equality Saturation. We present the tool, a...
CAV
2011
Springer
12 years 8 months ago
2011
Springer
Abstract. A fundamental question in the treatment of cardiac disorders, such as tachycardia and fibrillation, is under what circumstances does such a disorder arise? To answer to ...
CAV
2011
Springer
12 years 8 months ago
2011
Springer
Abstract. Many automatic testing, analysis, and verification techniques for programs can effectively be reduced to a constraint-generation phase followed by a constraint-solving ...
CAV
2011
Springer
12 years 8 months ago
2011
Springer
Abstract. Quantified Boolean formulae (QBF) allow compact encoding of many decision problems. Their importance motivated the development of fast QBF solvers. Certifying the result...
CAV
2011
Springer
12 years 8 months ago
2011
Springer
Abstract. We describe a tool that applies theorem proving technology to synthesize code fragments that use given library functions. To determine candidate code fragments, our appro...
CAV
2011
Springer
12 years 8 months ago
2011
Springer
Abstract. The underground malware-based economy is flourishing and it is evident that the classical ad-hoc signature detection methods are becoming insufficient. Malware authors ...
CAV
2011
Springer
12 years 8 months ago
2011
Springer
Abstract. BAP is a publicly available infrastructure for performing program verification and analysis tasks on binary (i.e., executable) code. In this paper, we describe BAP as we...