Skip to main content

4 Result(s)

within Florian Schanda Remove this filter

and

  1. Chapter and Conference Paper

    Building Better Bit-Blasting for Floating-Point Problems

    An effective approach to handling the theory of floating-point is to reduce it to the theory of bit-vectors. Implementing the required encodings is complex, error prone and requires a deep understanding of flo...

    Martin Brain, Florian Schanda, Youcheng Sun in Tools and Algorithms for the Construction … (2019)

    Download PDF (495 KB) View Chapter

  2. No Access

    Chapter and Conference Paper

    Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK

    This paper presents a retrospective of our experiences with applying theorem proving to the verification of SPARK programs, both in terms of projects and the technical evolution of the language and tools over ...

    Roderick Chapman, Florian Schanda in Interactive Theorem Proving (2014)

  3. No Access

    Chapter and Conference Paper

    Auditing User-Provided Axioms in Software Verification Conditions

    A common approach to formally checking assertions inserted into a program is to first generate verification conditions, logical sentences that, if then proven, ensure the assertions are correct. Sometimes user...

    Paul Jackson, Florian Schanda… in Formal Methods for Industrial Critical Sys… (2013)

  4. No Access

    Chapter and Conference Paper

    A Lightweight Technique for Distributed and Incremental Program Verification

    Applying automated verification to industrial code bases creates a significant computational task even when the individual conditions to be checked are trivial. This affects the wall clock time taken to verify...

    Martin Brain, Florian Schanda in Verified Software: Theories, Tools, Experiments (2012)