Workshop on Real Verification
Invited Speakers
- Cyril Cohen, Inria Sophia-Antipolis, France
- Jeehoon Kang, Seoul National University, Republic of Korea
- Johannes Kanig, AdaCore
- Sunyoung Kim, Yonsei University, Republic of Korea
- Michal Konečný, Aston University, United Kingdom-
- Norbert Müller, Universität Trier, Germany
- Sukyoung Ryu, KAIST, Republic of Korea
- Gyesik Lee, Hankyong National University, Republic of Korea
- Martin Ziegler, KAIST School of Computing, Republic of Korea
Conference Venue
Hosted and organized by
KAIST's School of Computing,
the conference will take place at N1 Building, Room #101 on
KAIST's Main Campus in Daejeon.
See CCA 2017 local information for details...
Schedule
- 9:15 registration/coffee
- 9:35 opening
- 9:45 Sunyoung Kim: Towards certified exact real computation
When we use computers to do computing with real numbers, it is likely that we
cannot guarantee the correctness of the results. In this talk, we give an
overview of our recent project about certified exact real arithmetic. The main
goal of our project is to develop and extend verified libraries for exact real
arithmetic.
- 10:30 Cyril Cohen: Real algebraic numbers in Coq
In this talk I describe a formalization in Coq of the set of real
algebraic numbers, together with a formal proof that this set has a
structure of discrete Archimedean real closed field. This work is
a basis for the construction of complex algebraic numbers and is
a reference implementation for the certification of numerous
algorithms relying on algebraic numbers in computer algebra.
- 11:15 coffee break
- 11:45 Michal Konečný: Exact real computation in AERN2/Haskell
We give an overview of the Haskell experimental library AERN2 and how it fits
our vision of providing tools for programming reliable and efficient exact
real number computation easily. We describe the main concepts and illustrate
them using examples, including a data type of analytic functions and a
parallel implementation of FFT. We demonstrate how the AERN2/Haskell type
system helps find programming errors as early as possible while not obscuring
the program.
- 12:30 Norbert Müller: Some Steps into Verification of Exact Real Arithmetic
The mathematical concept of real numbers is much richer than
the double precision numbers widely used as their implementation on a
computer. The field of `exact real arithmetic' tries to combine the elegance
and correctness of the mathematical theories with the speed of double
precision hardware, as far as possible.
In this talk, we describe an ongoing approach using the specification language
ACSL, the tool suite Frama-C and the proof assistant Coq to verify central
aspects of the iRRAM software package, which is known to be a fast
C++ implementation of `exact' reals numbers.
- 13:15 go to lunch
- 14:45 Jeehoon Kang: iRRAM-Coq: Fearless Verification of Exact Real Arithmetic Programs
Real numbers have so rich structure that they are usually represented in
lossy-compressed formats, e.g. floating-point ones, in computer programs.
However, arithmetic properties such as add's associativity are often broken in
these formats. In order to enjoy these elegant properties in programming,
runtime libraries for exact real arithmetic (ERA) are developed. However, due
to inherent complexity of real arithmetic, these libraries can provide only
comparison operators with error bounds, which complicate programming with ERA
and reasoning ERA programs.
In order to address this difficulty, we present iRRAM-Coq: a *program logic* on which one can reason ERA programs. iRRAM-Coq is *sound*: it is formally proved in the Coq proof assistant that if the logic says a program is correct, then the
program is actually correct. Thanks to the formally-verified soundness proof,
one can fearlessly reason about ERA programs without worrying about mistakes and
omissions. iRRAM-Coq is *executable*: an ERA program verified in iRRAM-Coq
can be extracted to C++ and then linked to the iRRAM runtime library for ERA.
As a case study, we successfully verified an integer-valued binary logarithm
function, extracted it to C++, and ran it.
- 15:30 coffee break
- 16:00 Sukyoung Ryu: Journey to Find Bugs in JavaScript Web Applications in the Wild
Analyzing real-world JavaScript web applications is a challenging task. On top
of understanding the semantics of JavaScript, it requires modeling of web
documents, platform objects, and interactions between them. In this talk, we
present our attempts to analyze JavaScript web applications in the wild mostly
statically using various approaches. From pure JavaScript programs to
JavaScript web applications using platform-specific libraries and dynamic code
loading, we explain technical challenges in analyzing each of them and how we
built an open-source analysis framework for JavaScript, SAFE, that addresses
the challenges incrementally. In spite of active research accomplishments in
analysis of JavaScript web applications, many issues still remain to be
resolved such as events, callback functions, and hybrid web applications. We
discuss possible future research directions and open challenges.
- 16:45 Johannes Kanig: SPARK - Formal Verification for the Software Engineer
SPARK is a formally verifiable subset of the Ada programming language. We give
a short overview over the SPARK language and tools, including a short
demonstration. We present the progress on the support of floating-point
arithmetic and will show examples of safety-critical systems that have been
developed with SPARK, and newer projects that are emerging in the community.
- 17:30 conclusion
Excursion
For foreign participants
there is a limited number of seats available
to an optional, final excursion
to Seoul on July 29 (Saturday);
particularly if your return flight leaves on Sunday:
Departure in the morning from Daejeon by bus,
lunch in a restaurant in Seoul,
guided tour of some king's palace(s).
First-come first-serve: