Name
Abstract | ||
|---|---|---|
This paper proposes a new approach for deriving invariants that are systems of congruence equations where the modulo is a power of 2. The technique is an amalgam of SAT-solving, where a propositional formula is used to encode the semantics of a basic block, and abstraction, where the solutions to the formula are systematically combined and summarised as a system of congruence equations. The resulting technique is more precise than existing congruence analyses since a single optimal transfer function is derived for a basic block as a whole. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-70545-1_26 | CAV |
Keywords | Field | DocType |
inferring congruence,congruence analysis,resulting technique,propositional formula,basic block,new approach,single optimal transfer function,congruence equation,transfer function | Abstraction,Computer science,Modulo,Algorithm,Basic block,Transfer function,Invariant (mathematics),Congruence (geometry),Propositional formula,Semantics | Conference |
Volume | ISSN | Citations |
5123 | 0302-9743 | 12 |
PageRank | References | Authors |
0.59 | 18 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andy King | 1 | 12 | 0.59 |
| Harald Søndergaard | 2 | 858 | 79.52 |