The Spec# Programming System: An Overview

By Mike Barnett, K. Rustan, M. Leino, Wolfram Schulte. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, 2004

1,202 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Hardware and Architecture, Software

View Paper: https://www.semanticscholar.org/paper/239e8f924eaefba08e461119a2eaebcd43e02247

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Hardware and Architecture

In Software

Citations in the corpus

A Survey of Automated Techniques for Formal Software Verification (2008, background): “They are useful for computing inequality constraints about integer variables and for deriving such invariants for nested program loops.”
Boogie: A Modular Reusable Verifier for Object-Oriented Programs (2005, background): “per [ BLS04 ]. The languages SPARK Ada [Bar03], B [Abr96], ACL2 [KMM00], Perfect Developer [Esc06], and C0 [LPP05] include verifiers with interactive theorem provers.”
Efficient E-Matching for SMT Solvers (2007, methodology): “It includes the SMT-LIB [27] AUFLIA/simplify, ESC/Java, and Boogie bench- marks.”
An overview of JML tools and applications (2003, methodology): “A more recent initiative that is very similar to JML is Spec# [6].”
ABS: A Core Language for Abstract Behavioral Specification (2010, background): “Examples of implementation-oriented specification languages are JML [8] and Spec# [7].”
Z3: An Efficient SMT Solver (2008, methodology): “Currently, Z3 is used in Spec#/Boogie [2,7], Pex [13], HAVOC [11], Vigi-lante [3], a verifying C compiler (VCC), and Yogi [10].”
Smallfoot: Modular Automatic Assertion Checking with Separation Logic (2005, background): “Work on ESC and Spec# has resulted in important advances on modular heap verification [16, 3].”
Growing solver-aided languages with rosette (2013, background): “ROSETTE builds on a rich body of prior work on solver-aided languages [5, 23–25, 27, 31, 34, 35] and symbolic evaluation [8, 10, 12, 15, 21, 37, 40].”
Why3: Shepherd Your Herd of Provers (2011, background): “In JML [10] or Spec# [2], for instance, such models are described using the pure fragment of the underlying programming language.”
VCC: A Practical System for Verifying Concurrent C (2009, methodology): “VCC reuses the Spec# tool chain [9], which has allowed developing a comprehensive C verifier with limited effort.”
Mop: an efficient and generic runtime verification framework (2007, background): “Spec# [10] is a DBClike extension of the object-oriented language C#.”
Improving the reliability of commodity operating systems (2005, methodology): “Recent language designs, such as ESP [124] and Spec] [18], allow model checking of executable code.”
Crying Wolf: An Empirical Study of SSL Warning Effectiveness (2009, background): “In the summer of 2008 we conducted an online survey of Internet users from around the world to determine how they perceived the current web browser SSL warnings.”