Travelled to:1 × France
1 × Germany
1 × Japan
2 × The Netherlands
2 × USA
Collaborated with:N.Ghani B.Wolff S.Autexier D.Walter ∅ M.Abbott H.Tej Kolyang B.Krieg-Brückner K.0001 T.M.0001
Talks about:program (5) theorem (3) develop (3) win (3) tas (3) isa (3) transform (2) formal (2) verif (2) prove (2)
Person: Christoph Lüth
DBLP: L=uuml=th:Christoph
Contributed to:
2010
2009
2005
2002
200019991996
1997Wrote 8 papers:
- IFM-2010-AutexierL #c #impact analysis #source code #verification
- Adding Change Impact Analysis to the Formal Verification of C Programs (SA, CL), pp. 59–73.
- FM-2009-LuthW #c #source code #specification #verification
- Certifiable Specification and Verification of C Programs (CL, DW), pp. 419–434.
- RTA-2005-AbbottGL #composition
- Abstract Modularity (MA, NG, CL), pp. 46–60.
- ICFP-2002-LuthG #monad #using
- Composing monads using coproducts (CL, NG), pp. 133–144.
- FASE-2000-LuthW #development #tool support
- More About TAS and IsaWin — Tools for Formal Program Development (CL, BW), pp. 367–370.
- FASE-1999-LuthTKK #development #proving #theorem proving #tool support
- TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving (CL, HT, K, BKB), pp. 239–243.
- RTA-1996-Luth #algebra #composition #proving #term rewriting #theorem
- Compositional Term Rewriting: An Algebraic Proof of Toyama’s Theorem (CL), pp. 261–275.
- TAPSOFT-1997-KolyangLMW #development #interface #proving #theorem proving
- TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving (K0, CL, TM0, BW), pp. 855–858.