| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Practical Aspects of Automated Deduction for Program Verification
- 2010
-
Ingår i: KI - K√ºnstliche Intelligenz. - : Springer Science and Business Media LLC. - 0933-1875 .- 1610-1987. ; 24:1, s. 43-49
-
Tidskriftsartikel (refereegranskat)abstract
- Software is vital for modern society. It is used in manysafety- or security-critical applications, where a high degree of correctness is desirable. Over the last years, technologies for the formal specification and verification of software -- using logic-based specification languages and automated deduction -- have matured and can be expected to complement and partly replace traditional software engineering methods in the future. Program verification is an increasingly important application area for automated deduction. The field has outgrown the area of academic case studies, and industry is showing serious interest. This article describes the aspects of automated deduction that are important for program verification in practice, and it gives an overview of the reasoning mechanisms, the methodology, and the architecture of modern program verification systems.
|
|
| 2. |
- Arlt, Stephan, et al.
(författare)
-
The Gradual Verifier
- 2014
-
Ingår i: NASA Formal Methods. - Switzerland : Springer International Publishing. - 9783319061993 ; , s. 313-327
-
Konferensbidrag (refereegranskat)
|
|
| 3. |
- Felsing, Dennis, et al.
(författare)
-
Automating regression verification
- 2014
-
Ingår i: ASE '14 Proceedings of the 29th ACM/IEEE international conference on Automated software engineering. - New York : ACM Press. - 9781450330138 ; , s. 349-360
-
Konferensbidrag (refereegranskat)
|
|
| 4. |
|
|
| 5. |
- Zeljic, Aleksandar, et al.
(författare)
-
Approximations for Model Construction
- 2014
-
Ingår i: Automated Reasoning. - Cham : Springer. - 9783319085869 - 9783319085876 ; , s. 344-359
-
Konferensbidrag (refereegranskat)abstract
- We consider the problem of efficiently computing models for satisfiable constraints, in the presence of complex background theories such as floating-point arithmetic. Model construction has various applications, for instance the automatic generation of test inputs. It is well-known that naive encoding of constraints into simpler theories (for instance, bit-vectors or propositional logic) can lead to a drastic increase in size, and be unsatisfactory in terms of memory and runtime needed for model construction. We define a framework for systematic application of approximations in order to speed up model construction. Our method is more general than previous techniques in the sense that approximations that are neither under- nor over-approximations can be used, and shows promising results in practice.
|
|
