Browsing by Author "Lim, Junghee"
Now showing items 5-9 of 9
-
MCDASH: Refinement-Based Property Verification for Machine Code
Lal, Akash; Lim, Junghee; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2009)This paper presents MCDASH, a refinement-based model checker for machine code. While model checkers such as SLAM, BLAST, and DASH have each made significant contributions in the field of verification/flaw-detection, ... -
PostHat and All That: Attaining Most-Precise Inductive Invariants
Reps, Thomas; Lim, Junghee; Lal, Akash; Thakur, Aditya (2013-04-16)In abstract interpretation, the choice of an abstract domain fixes a limit on the precision of the inductive invariants that one can express; however, for a given abstract domain A, there is a most-precise (``strongest'', ... -
Symbolic Analysis via Semantic Reinterpretation
Lim, Junghee; Lal, Akash; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2008)In recent years, the use of symbolic analysis in systems for testing and verifying programs has experienced a resurgence. By ``symbolic program analysis'', we mean logic-based techniques to analyze state changes along ... -
A System for Generating Static Analyzers for Machine Instructions
Lim, Junghee; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2007)There is growing interest in analyzing executables to look for bugs and security vulnerabilities. This paper describes the design and implementation of a language for describing the semantics of an instruction set, along ... -
TSL: A System for Generating Abstract Interpreters and its Application to Machine-Code Analysis
Lim, Junghee; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2012-10-02)This paper describes the design and implementation of a system, called TSL (for "Transformer Specification Language"), that provides a systematic solution to the problem of creating retargetable tools for analyzing machine ...