Programming languages and software engineering
Project
Boogie: An Intermediate Verification Language
Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for…
Project
Model-based Testing with SpecExplorer
Spec Explorer is a software development tool for advanced model-based specification and conformance testing. New Version of Spec Explorer as an extension to Visual Studio is now available: Spec Explorer 2010 What are the…
Project
FORMULA – Modeling Foundations
FORMULA 2.0: Formal Specifications for Verification and Synthesis Formula specifications are highly declarative logic programs that can express rich synthesis and verification problems. FORMULA 2.0 is framework for formally specifying domain-specific languages (DSLs) and model…
Project
VCC: A Verifier for Concurrent C
VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated…
Publication
Programming Languages and Systems
Project
Detection of JavaScript-based Malware
Nozzle: Runtime heap spray detector Nozzle is a runtime monitoring infrastructure that detects attempts by attackers to spray the heap. Nozzle uses lightweight emulation techniques to detect the presence of objects that contain executable code. To…
Project
VS3 (Verification and Specification using SMT Solvers)
SMT Solvers have traditionally been used for verifying correctness of systems that have been annotated with relevant inductive invariants. Such an annotation usually is an undesirable burden on the user. This project explores techniques for…
Project
SPEED (Symbolic Resource Time/Space Bounds Analysis)
Introduction Performance measurement of software is a critical component of software development. Performance is traditionally measured using profiling, which is often too little (only certain inputs are profiled) or too late (to make requisite changes…