Microsoft Research, USA
From Retrospective Verification to Forward-Looking Development
One obstacle in applying program verification is coming up with specifications. That is, if you want to verify a program, you need to write down what it means for the program to be correct. But doesn't that seem terribly wrong? Why don't we see it as "one obstacle in program design is coming up with code"? That is, if you want to realize a specification, you need to write down how the machine is supposed do it. Phrased this way, we may want to change our efforts of verification into efforts of what is known as correct-by-construction or stepwise-refinement. But the choice is not so clear and there are plenty of obstacles on both sides. For example, many programs are developed from specifications, but the specifications are not in a form suitable for refinement tools. For other programs, the clearest specifications may be given by pseudo-code, but such specification may not be suitable for some verification tools. In this talk, I will discuss verification tools and refinement-based tools, considering how they may be combined.
Do Coding Standards improve Software Quality?
Many organisations require developers to adhere to a coding standard that consists of rules of good practice. The rules may range from naming conventions to avoidance of common programming errors. A well-known example is the Joint Strike Fighter (JSF) standard for C++. Coding standards like JSF are enforced via code reviews and automated checkers. How effective are coding standards in improving code quality? Can we determine whether one set of rules is more effective than another? In this talk we shall explore these questions with reference to a number of large-scale projects.
Software Engineering Chair
Saarland University, Germany
Specifications for Free
Recent advances in software validation and verification make it possible to widely automate the check whether a specification is satisfied. This progress is hampered, though, by the persistent difficulty of writing specifications. Are we facing a "specification crisis"? By mining specifications from existing systems, we can alleviate this burden, reusing and extending the knowledge of 60 years of programming, and bridging the gap between formal methods and real-world software. In this talk, I present the state of the art in specification mining, its challenges, and its potential, up to a vision of seamless integration of specification and programming.