up: Martin Strecker

Martin Strecker: Publications

in reverse chronological order. Also see my DBLP entries

A. Mahajan, M. Strecker, MW. Wong:
Overview of the CCLAW L4 project,
ProLaLa 2022
J.H. Brenas, R. Echahed, M. Strecker:
Verifying Graph Transformations with Guarded Logics,
TASE 2018
J.H. Brenas, R. Echahed, M. Strecker:
Reasoning Formally about Database Queries and Updates,
FM 2019
M. Strecker
Interactive and automated proofs for graph transformations
M. Strecker
Deciding extended modal logics by combining state space generation and SAT solving
J.H. Brenas, R. Echahed, M. Strecker
Verifying Graph Transformation Systems with Description Logics
J.H. Brenas, R. Echahed, M. Strecker
C2PDLS: A Combination of Combinatory and Converse PDL with Substitutions
J.H. Brenas, R. Echahed, M. Strecker
On the Closure of Description Logics under Substitutions
J.H. Brenas, R. Echahed, M. Strecker
Ensuring Correctness of Model Transformations While Remaining Decidable
J.H. Brenas, R. Echahed, M. Strecker
Proving Correctness of Logically Decorated Graph Rewriting Systems
A. Makhlouf, H.N. Tran, Ch. Percebois, M. Strecker
Combining Dynamic and Static Analysis to Help Develop Correct Graph Transformations
N. Baklanova, J.H. Brenas, R. Echahed, Ch. Percebois, M. Strecker, H.N. Tran
Provably Correct Graph Transformations with Small-tALC
N. Baklanova, W. Ricciotti, J.-G. Smaus, M. Strecker
Abstracting an operational semantics to finite automata
J.-H. Brenas, R. Echahed, M. Strecker
A Hoare-like calculus using the SROIQσ logic on transformations of graphs
J.-H. Brenas, R. Echahed, M. Strecker
SROIQσ is decidable
J.-H. Brenas, M. Chaabani, R. Echahed, M. Strecker
Logical foundations for reasoning about transformations of knowledge bases
C. Percebois, M. Strecker, H. Nhi Tran
Rule-level verification of graph transformations for invariants based on edges' transitive closure
S. Djeddai, M. Strecker, M. Mezghiche
Integrating a Formal Development for DSLs into Meta-modeling
M. Giorgino, M. Strecker
Correctness of pointer manipulating algorithms illustrated by a verified BDD construction
N. Baklanova, M. Strecker
Abstraction and Verification of Properties of a Real-Time Java
S. Djeddai, M. Mezghiche, M. Strecker
A Case Study in Combining Formal Verification and Model-Driven Engineering
N. Baklanova, M. Strecker, L. Féraud
Resource Sharing Conflicts Checking in Multithreaded Java Programs
M. Strecker
Locality in Reasoning about Graph Transformations
O. Gasquet, F. Schwarzentruber, M. Strecker
Panda: A Proof Assistant in Natural Deduction for All
O. Gasquet, F. Schwarzentruber, M. Strecker
Satoulouse: The Computational Power of Propositional Logic Shown to Beginners
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: Sat Feb 26 23:00:15 CET 2022