Abstract:

With growing dependence on software in embedded and cyber-physical systems where vulnerabilities and malware can lead to disasters, efficient and accurate verification has become a crucial need for safety and cybersecurity. Formal verification of large software has remained an elusive target, riddled with problems of low accuracy and high computational complexity. The need for automating verification is undoubted, however human is indispensable to accurate real-world software verification. The automation should actually enable and simplify human crosschecking, which is especially important when the stakes are high. This technical briefing discusses the challenges of creating a powerful fusion of automation and human intelligence to solve software verification problems where complete automation has remained intractable. We will contrast with existing software verification approaches and reflect on their strengths and limitations as a human-machine collaboration framework and outline key software engineering research and practice challenges to be addressed in the future.

Venue: 38th International Conference on Software Engineering (ICSE 2016), Austin, Texas, May 14-22, 2016

Authors: Suresh Kothari, Ahmed Tamrawi, Jon Mathews

Paper (PDF): RethinkingVerification-ICSE2016.pdf

Bibtex:
@inproceedings{Kothari:2016:RVA:2889160.2891046,
author = {Kothari, Suresh and Tamrawi, Ahmed and Mathews, Jon},
title = {Rethinking Verification: Accuracy, Efficiency and Scalability Through Human-machine Collaboration},
booktitle = {Proceedings of the 38th International Conference on Software Engineering Companion},
series = {ICSE '16},
year = {2016},
isbn = {978-1-4503-4205-6},
location = {Austin, Texas},
pages = {885--886},
numpages = {2},
url = {http://doi.acm.org/10.1145/2889160.2891046},
doi = {10.1145/2889160.2891046},
acmid = {2891046},
publisher = {ACM},
address = {New York, NY, USA},
}