Sciweavers

FAC
2007
170views more  FAC 2007»
13 years 11 months ago
Are the Logical Foundations of Verifying Compiler Prototypes Matching user Expectations?
Abstract. The Verifying Compiler (VC) project proposals suggest that mainstream software developers are its targeted end-users. Like other software engineering efforts, the VC proj...
Patrice Chalin
ASIAN
2006
Springer
153views Algorithms» more  ASIAN 2006»
14 years 3 months ago
Automata-Based Confidentiality Monitoring
Abstract Non-interference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. In contrast to static checkin...
Gurvan Le Guernic, Anindya Banerjee, Thomas P. Jen...
CASSIS
2004
Springer
14 years 4 months ago
ESC/Java2: Uniting ESC/Java and JML
The ESC/Java tool was a lauded advance in effective static checking of realistic Java programs, but has become out-of-date with respect to Java and the Java Modeling Language (JML...
David R. Cok, Joseph Kiniry
SEFM
2005
IEEE
14 years 5 months ago
Omnibus Verification Policies: A flexible, configurable approach to assertion-based software verification
The three main assertion-based verification approaches are: Design by Contract (DBC), Extended Static Checking (ESC) and Verified Design by Contract (VDBC). Each approach offers a...
Thomas Wilson, Savi Maharaj, Robert G. Clark
ICECCS
2006
IEEE
90views Hardware» more  ICECCS 2006»
14 years 5 months ago
A Type System for the Relational Calculus of Object Systems
Being a successful technique in software practice, Object Orientation (OO) is a hot topic in academic research fields. Among many formalisms, rCOS, a refinement calculus of obje...
Liang Zhao, Xiangpeng Zhao, Quan Long, Zongyan Qiu
ICSE
2009
IEEE-ACM
14 years 6 months ago
Exploiting the synergy between automated-test-generation and programming-by-contract
This demonstration presents two tools, Code Contracts and Pex, that utilize specification constructs for advanced testing, runtime checking, and static checking of object-oriente...
Michael Barnett, Manuel Fähndrich, Peli de Ha...
ICSE
2005
IEEE-ACM
14 years 11 months ago
Check 'n' crash: combining static checking and testing
We present an automatic error-detection approach that combines static checking and concrete test-case generation. Our approach consists of taking the abstract error conditions inf...
Christoph Csallner, Yannis Smaragdakis
SIGSOFT
2002
ACM
15 years 7 days ago
Invariant inference for static checking
Static checking can verify the absence of errors in a program, but often requires written annotations or specifications. As a result, static checking can be difficult to use effec...
Jeremy W. Nimmer, Michael D. Ernst