Abstract | ||
---|---|---|
We define an abstraction of the continuous variables that serve as inputs to embedded software. In existing static analyzers, these variables are most often abstracted by a constant interval, and this approach has shown its limits. We propose a different method that analyzes in a more precise way the continuous environment. This environment is first expressed as the semantics of a special continuous program, and we define a safe abstract semantics. We introduce the abstract domain of interval valued step functions and show that it safely over-approximates the set of continuous functions. The theory of guaranteed integration is then used to effectively compute an abstract semantics and we prove that this abstract semantics is safe. |
Year | DOI | Venue |
---|---|---|
2008 | 10.1007/978-3-540-78163-9_8 | VMCAI |
Keywords | Field | DocType |
embedded program,constant interval,special continuous program,abstract domain,continuous function,abstract interpretation,embedded software,continuous variable,different method,continuous environment,abstract semantics,physical input,safe abstract semantics | Continuous function,Programming language,Abstraction,Embedded software,Abstract interpretation,Computer science,Theoretical computer science,Hybrid system,Semantics,Step function,Hybrid automaton | Conference |
Volume | ISSN | ISBN |
4905 | 0302-9743 | 3-540-78162-5 |
Citations | PageRank | References |
4 | 0.47 | 17 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Olivier Bouissou | 1 | 123 | 9.52 |
Matthieu Martel | 2 | 299 | 27.39 |