Computer Science Logic and 8th Kurt Gödel Colloquium
Helmut Veith: Friends or Foes? Communities in Software Verification
Welcome and News
Host Institutions
Calls and Deadlines
Program
Social Program
Registration
Location and Venue
Accommodation
Committees
Contact
Colocated Events
Authors' instructions
Print current pagePrint this page
In contrast to hardware which is finite-state and based on relatively few ample principles, software systems generally give rise to infinite state spaces, and are described in terms of programming languages involving rich semantical concepts. The challenges of software verification can be addressed only by a combined effort of different communities including, most notably, model checking, theorem proving, symbolic computation, static analysis, compilers, and abstract interpretation. We focus on a recent family of tools which use predicate abstraction and theorem proving to extract a finite state system amenable to model checking.
© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-07-09 Valid HTML 4.01! Valid CSS! Debian