Sciweavers

VSTTE
2005
Springer
13 years 10 months ago
Tool Integration for Reasoned Programming
We argue for the importance of tool integration in achieving the Program Verifier Grand Challenge. In particular, we argue for what we call strong integration, i.e. a co-operative...
Andrew Ireland
VSTTE
2005
Springer
13 years 10 months ago
It Is Time to Mechanize Programming Language Metatheory
How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and p...
Benjamin C. Pierce, Peter Sewell, Stephanie Weiric...
VSTTE
2005
Springer
13 years 10 months ago
Reliable Software Systems Design: Defect Prevention, Detection, and Containment
The grand challenge that is the focus of this conference targets the development of a practical methodology for software verification: a methodology that can help us to reduce the ...
Gerard J. Holzmann, Rajeev Joshi
VSTTE
2005
Springer
13 years 10 months ago
Performance Validation on Multicore Mobile Devices
The validation of modern software systems on mobile devices needs to incorporate both functional and non-functional requirements. While some progress has been made in validating pe...
Thomas Hubbard, Raimondas Lencevicius, Edu Metz, G...
VSTTE
2005
Springer
13 years 10 months ago
Linking the Meaning of Programs to What the Compiler Can Verify
We formulate some research and development challenges that relate what a verifying compiler can verify to the definition and analysis of the application-content of programs, where...
Egon Börger
VSTTE
2005
Springer
13 years 10 months ago
Model-Checking Software Using Precise Abstractions
Marsha Chechik, Arie Gurfinkel
VSTTE
2005
Springer
13 years 10 months ago
Specified Blocks
This paper argues that specified blocks have every advantage over the combination of assertions, preconditions, postconditions, invariants, and variants, both for verifying program...
Eric C. R. Hehner
VSTTE
2005
Springer
13 years 10 months ago
From the How to the What
In this paper, we consider the Grand Challenge under a very specific perspective: the enabling of application experts without programming knowledge to reliably model their busines...
Tiziana Margaria, Bernhard Steffen
VSTTE
2005
Springer
13 years 10 months ago
Model Checking: Back and Forth between Hardware and Software
The interplay back and forth between software model checking and hardware model checking has been fruitful for both. Originally intended for the analysis of concurrent software, mo...
Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, He...