up: Martin Strecker

Martin Strecker: Publications

in reverse chronological order (also see publications database of the IRIT)

M. Strecker
Interactive and automated proofs for graph transformations
N. Baklanova, M. Strecker, L. Féraud
Resource Sharing Conflicts Checking in Multithreaded Java Programs
M. Strecker
Locality in Reasoning about Graph Transformations
M. Giorgino, M. Strecker
BDDs verified in a proof assistant (Preliminary report)
M. Chaabani, M. Mezghiche, M. Strecker
Vérification d'une méthode de preuve pour la logique de description ALC
M. Giorgino, M. Strecker, R. Matthes, M. Pantel
Verification of the Schorr-Waite algorithm - From trees to graphs
M. Strecker
Clock type soundness in synchronous languages
M. Chaabani, M. Mezghiche, M. Strecker
Formalisation de la logique de description ALC dans l'assistant de preuve Coq
M. Giorgino, R. Matthes, M. Strecker
Génération de programmes efficaces et vérifiés
N. Izerrouken, X. Thirioux, M. Pantel, M. Strecker
Certifying an Automated Code Generator Using Formal Tools : Preliminary Experiments in the GeneAuto Project
R. Matthes, M. Strecker
Verification of the Redecoration Algorithm for Triangular Matrices
M. Strecker
Modeling and Verifying Graph Transformations in Proof Assistants
M. Strecker, M. Giorgino
Towards a Formalisation of Graph Transformations in Proof Assistants
Jean-Paul Bodeveix, David Chemouil, Mamoun Filali, Nicolas Lalevee, Martin Strecker
Towards the verification of model transformations
J.P. Bodeveix, D. Chemouil, M. Filali, M. Strecker
Towards formalising AADL in Proof Assistants
M. Strecker
Compiler Verification for C0 (intermediate report)
G. Klein, M. Strecker
Verified Bytecode Verification and Type-Certifying Compilation
Journal of Logic and Algebraic Programming
M. Strecker
Formal Analysis of an Information Flow Type System for MicroJava
available as short version and technical report
B. Schätz, J. Romberg, M. Strecker, O. Slotosch, K. Spies, et. al.
Modeling Embedded Software: State of the Art and Beyond
In: Proc. ICSSEA 2003
B. Schätz, J. Romberg, M. Strecker, O. Slotosch, K. Spies, et. al.
CASE Tools for Embedded Systems
TUM technical report
S. Berghofer, M. Strecker
Extracting a formally verified, fully executable compiler from a proof assistant
In Proc. COCV'2003
M. Strecker
Investigating Type-Certifying Compilation with Isabelle
In Proc. LPAR'02
M. Strecker
Formal Verification of a Java Compiler in Isabelle
In Proc. of CADE'02
M. Strecker
Construction and Deduction in Type Theories
Ph.D. University of Ulm, 1999
M. Strecker, M. Luther, F. W. von Henke
Interactive and automated proof construction in type theory
In: Automated Deduction - A Basis for Applications, W. Bibel und P. Schmitt, Kluwer Academic Publishers, 1998.
Volume I: Foundations, Chapter 3: Interactive Theorem Proving.
M. Luther, M. Strecker
A guided tour through Typelab
Technical Report UIB-98-03, Universität Ulm, Fakultät für Informatik, Jan. 1998
M. Strecker, M. Luther, F.W. von Henke
Typelab: An Environment for Modular Program Development
Proc. of TAPnSOFT'97, Springer LNCS 1214, pp. 851-854, 1997
M. Strecker, M. Sorea
Integrating an Equality Prover into a Software Development System based on Type Theory
Proc. of KI'97, Springer LNAI 1303, pp. 147-158, 1997
F.W. von Henke, M. Luther, H. Pfeifer, H. Rueß, D. Schwier, M. Strecker, M. Wagner
The Typelab Specification and Verification Environment
Proc. of AMAST'96, Springer LNCS 1101, pp. 604-607, Munich, 1996
M. Strecker, M. Luther, M. Wagner
Structuring and Using a Knowledge Base of Mathematical Concepts: A Type-Theoretic Approach
Proc. of ECAI'96, pp. 23-26, 1996
F.W. von Henke, A. Dold , H. Rueß, D. Schwier, and M. Strecker
Construction and Deduction Methods for the Formal Development of Software
in KORSO: Methods, Languages, and Tools for the Construction of Correct Software
Springer LNCS 1009, 1995.

Last modified: Thu Jul 30 11:41:25 CEST 2009