Tutorial 1
Parameterized Unit Testing with Pex
Jonathan de Halleux and Nikolai Tillmann
Microsoft Research, One Microsoft Way, Redmond, USA
This hands-on tutorial will teach the principles of parameterized unit testing with Pex, an automatic test input generator http://research.microsoft.com/pex.
A parameterized unit test (PUT) is simply a method that takes parameters, calls the code under test, and states assertions. Given a PUT written in a .NET language, Pex automatically produces a small test suite with high code and assertion coverage. Moreover, when a generated test fails, Pex can often suggest a bug fix. To do so Pex performs a systematic program analysis, similar to path bounded modelchecking. Pex learns the program behavior by monitoring execution traces, and uses a constraint solver to produce new test cases with different behavior. We have applied Pex to code developed at Microsoft, uncovering known and unknown bugs, including security-critical bugs, in shipped and unshipped products.
From a specification, the student will go through the steps of (1) writing PUTs in C# to reflect the specification, and (2) developing code that implements the specification. The tutorial will outline key aspects to make this methodology successful in practice, e.g. how to write mock objects, as well as the theoretical foundations on which Pex is built.
Tutorial 2
Integrating Verification and Testing of Object-Oriented Software
Christian Engel1, Christoph Gladisch2, Vladimir Klebanov2, Philipp Rümmer3
1)University of Karlsruhe (Germany), 2)University of Koblenz (Germany), 3)Chalmers University of Technology (Gothenburg, Sweden)
(tutorial website...)
Formal methods can only gain widespread use in industrial software
development if they are integrated:
- into software development techniques, tools, and languages used in practice
- with each other.
A symbiosis of software testing and verification techniques is a highly
desired goal, but at the current state of the art most available tools
are dedicated to just one of the two tasks: verification or testing. We
use the KeY system 1.0 (developed by the tutorial presenters) to
demonstrate our approach in combining both.
KeY is an integrated deductive verification environment that allows
full-functional verification of programs written in the industrial
object-oriented language Java Card. At the core of the system is a novel
interactive/automated theorem prover for the Dynamic Logic for Java. The
prover has an easy-to-use graphical interface and seamlessly integrates
automated and interactive proving. On the software development side, the
system offers plug-ins for the industrial platforms Borland Together and
Eclipse.
The KeY project is constantly working on techniques to increase the
returns of verification in the industrial setting, including: proof
reuse, symbolic debugging and verification-based testing.
The tutorial will cover the following topics:
- How to design and formally specify object-oriented software
(different fomalisms: UML/OCL, JML; tool support)
- Deductive analysis of designs and specifications in the KeY prover
- Deductive verification of non-trivial Java implementations with
the KeY prover
- Integration of verification and testing - why and how; generating
JUnit tests from proofs
