Intelligent Systems and Formal Methods in Software Engineering

Over the last few years, technologies for the formal description, construction, analysis, and validation of software - based mostly on logics and formal reasoning - have matured. We can expect them to complement and partly replace traditional software engineering methods in the future. Formal methods in software engineering are an increasingly important application area for intelligent systems. The field has outgrown the area of academic case studies, and industry is showing serious interest. We convincingly argue that we've reached the point where we can solve the problem of how to formally verify industrial-scale software. We propose program verification as a computer science Grand Challenge. Deductive software verification is a core technology of formal methods. We describe recent dramatic changes in the way it's perceived and used. Another important base technique of formal methods, besides software verification, is synthesizing software that's correct by construction because it's formally derived from its specification. We discuss recent developments and trends in this area. Surprisingly efficient decision procedures for the satisfiability modulo theories problem have recently emerged. We explain these techniques and why they're important for all formal-methods tools. We look at formal methods from an industry perspective. We explain the success of Microsoft Research's SLAM project, which has developed a verification tool for device drivers

Authors

• Bernhard Beckert Karlsruhe Institute of Technology
• Tony Hoare
• Reiner Hahnle
• Douglas Smith
• Cordell Green
• Silvio Ranise
• Cesare Tinelli
• Thomas Ball
• Sriram Rajamani Microsoft Research

Keywords

• Intelligent systems
• Software engineering
• Costs
• Application software
• Programming profession
• Computer science
• Computer errors
• Humans
• Energy management
• Financial management
• Formal Methods
• Grand Challenge
• Essential Step
• Programming Language
• Specific Language
• Language Model
• General Tool
• Human Genome Project
• Static Analysis
• Target Language
• Automatic Generation
• Target Program
• Code Generation
• Software Architecture
• Model Checking
• Smart Card
• Formal Verification
• Kestrel
• Domain-specific Languages
• Verification Tool
• Verification Of Conditions
• Authentication Protocol
• Starting State
• Value Creation
• Knowledge Representation
• First-order Logic
• Decision Problem
• Code Execution
• Correction Algorithm
• program verification
• deductive software verification
• satisfiability modulo theories
• software synthesis