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 ...