Concern-specific specification and verification to improve software quality
Project supervisors: Frank
Piessens, Wouter Joosen, Pierre Verbaeten
Desmet, Bart Jacobs, Jan
Smans, Dries Vanoverberghe
Formal methods have long been recognized as an important tool to help ensure quality of software.
In this research track we focus on the use of formal specification and
verification techniques to eradicate certain classes of bugs. Examples of the
classes of bugs that we target are concurrency related bugs and security related
Our approach consists of the design of concern-specific annotations,
whose formal semantics is defined by translation to existing general-purpose
specification languages such as Spec# and
JML. If the translated program +
specification verifies, we show that the original annotated program does not
exhibit a specific type of erroneous behavior.
We have instantiated this idea in three different settings:
- to deal with concurrency related bugs (data races and deadlocks), as described in detail in the
- B. Jacobs, K. R. M. Leino, F. Piessens, and W. Schulte, Safe concurrency for aggregate objects with invariants, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods
(Aichernig, B.K. and Beckert, B., eds.), pp. 137-146, 2005
- B. Jacobs, J. Smans, F. Piessens, and W. Schulte, A Statically Verifiable Programming Model for Concurrent Object-Oriented
To be presented at the Eighth International Conference on Formal Engineering Methods (ICFEM 2006), Macau, October 29-November 3, 2006.
- to deal with stack-inspection based sandboxing related bugs, as described in detail in the
- J. Smans, B.
Jacobs, and F. Piessens, Static
Verification of Code Access Security Policy Compliance of .NET
Applications, Journal of Object Technology 5 (3), pp.
35-58, April, 2006.
- J. Smans, B. Jacobs, and F. Piessens, Static verification of code access
security policy compliance of .NET applications, Proceedings of the 3rd
International Conference on .NET (Skala, V. and Nienaltowksi, P., eds.), pp.
- to deal with data dependency related bugs as described in detail in the
- L. Desmet, F. Piessens, W. Joosen, and P. Verbaeten, Static
Verification of Indirect Data Sharing in Loosely-coupled Component
Systems. In SC 2006, (W. Löwe and M. Südholt, eds.), vol. 4089/2006,
Lecture Notes in Computer Science, Springer-Verlag Berlin Heidelberg,
- L. Desmet, F. Piessens, W. Joosen, and P. Verbaeten, Bridging the Gap
Between Web Application Firewalls and Web Applications. Accepted at
Formal Methods in Security Engineering (FMSE'06), November 3,
Alexandria, Virginia, USA.