License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2015.3
URN: urn:nbn:de:0030-drops-52141
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5214/
Go to the corresponding LIPIcs Volume Portal

Summers, Alexander J.

Software Verification "Across the Stack" (Invited Talk)

pdf-format:
3.pdf (0.2 MB)

Abstract

Producing reliable programs has always been tough, and the complexity and variety of programming tasks just keeps on growing. Fortunately, the growth of computing power has also enabled substantial advances in automated reasoning, particularly the development of SMT solvers and automatic theorem provers. In turn, this has resulted in new research directions for program correctness, with the aim of producing tools which can verify complex properties of software automatically.

Developing useful verification techniques requires balancing a number of competing factors. We want to be as expressive as possible in the program properties we can support - if we can write it down, we'd like to be able to prove it. But to progress beyond pen-and-paper efforts, we also need to tailor our approaches such that they can be implemented or encoded by tools, ideally with both precise and efficient results. To make things harder still, if we hope to produce tools which everyday programmers can benefit from, we also need techniques that require manageable interaction from a user, and give understandable feedback.

In this talk, I'll describe some of the fun experiences I've had working on these kinds of problems, from the design of front-end program logics and reasoning techniques to the development of underlying implementation technology, and the tricky encoding challenges that show up in between.

BibTeX - Entry

@InProceedings{summers:LIPIcs:2015:5214,
  author =	{Alexander J. Summers},
  title =	{{Software Verification "Across the Stack" (Invited Talk)}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{3--3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{John Tang Boyland},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5214},
  URN =		{urn:nbn:de:0030-drops-52141},
  doi =		{10.4230/LIPIcs.ECOOP.2015.3},
  annote =	{Keywords: software verification, program logic, automatic verifier, program correctness, SMT solvers}
}

Keywords: software verification, program logic, automatic verifier, program correctness, SMT solvers
Collection: 29th European Conference on Object-Oriented Programming (ECOOP 2015)
Issue Date: 2015
Date of publication: 29.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI