Publications (chronologically ordered):


Copyright Notice: This material is presented to ensure, timely and most widely, the dissemination of scholarly and technical work. Copyright and all rights therein are retained by the authors or by other copyright holders, such as publishers. All persons copying this information are expected to adhere to the terms and constraints invoked by each copyright holder. In most cases, these works may not be reposted without explicit permission of the copyright holder.

2018

  • M. Mendler, J. Aguado, B. Bodin, P. Roop, R. von Hanxleden: Logic Meets Algebra: Compositional Timing Analysis for Synchronous Reactive Multithreading.(596.1 KB) To appear in: Festschrift on the Occasion of Bernhard Steffens's 60 Birthday: Models, Mindsets, Meta: The What, the How, and the Why Not? T. Margaria, S. Graf and K.G. Larsen (eds), Springer LNCS N 11200, 2018.
  • A. Schulz-Rosengarten, S. Smyth, R. von Hanxleden, M. Mendler: A Sequentially Constructive
    Circuit Semantics for Esterel
    . In: 18th International Conference on Applications of Concurrency to System Design (ACSD 2018), Bratislava, Slovakia, June 24-29, 2018.
  • J. Aguado, M. Mendler, M. Pouzet, P. Roop, R. von Hanxleden: Deterministic Concurrency -
    A Clock-Synchronised Shared Memory Approach.
    (682.4 KB) In Proc. 27th European Symposium on Programming (ESOP 2018), Thessaloniki, April 14-20, 2018.
  • A. Schulz-Rosengarten, S. Smyth, R. von Hanxleden, M. Mendler: A Sequentially Constructive
    Circuit Semantics for Esterel
    . Technical Report Nr. 1801, The Christian-Albrechts University of Kiel, Institut für Informatik, February 2018 (52 pages).

2017

  • J. Aguado, M. Mendler, M. Pouzet, P. Roop and R. von Hanxleden: Clock-Synchronised Shared Objects for Deterministic Concurrency.(1.5 MB)Technical Report, Faculty of Information Systems and Applied Computer Sciences, Bamberg University, No. 102, July 2017. Updated Version: April 2018 (86 pages).
  • J. Aguado, M. Mendler, J. J. Wang, B. Bodin and P. Roop: Compositional Timing-Aware Semantics for Synchronous Programming. In Proc. Forum on Specification & Design Languages (FDL 2017), Verona, Italy, September 2017.
  • A. Malik, P. Roop, S. Andalam, M. Trew and M. Mendler: Modular compilation of hybrid systems for emulation and large scale simulation. In Proc. International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES 2017), Seoul, South Korea, October 2017. ACM Transactions on Embedded Systems, Vol. 16 (5s), October 2017.
  • J. Wang, M. Mendler, P. Roop and B. Bodin: Timing analysis of synchronous programs using WCRT Algebra: Scalability through abstraction. In Proc. International Confeence on Embedded Software (EMSOFT 2017), Seoul, South Korea October 2017. Vol. 16 (5s), October 2017.
  • S. Smyth, Chr. Motika, K. Rathlev, R. von Hanxleden, M. Mendler: SCEst: Sequentially Constructive Esterel. To appear in ACM Transactions on Embedded Computing Systems.

2016

  • M. Mendler, P. S. Roop, B. Bodin: A novel WCET semantics of synchronous programs. In Proc. 4th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2016), Quebec, Canada, August 2016. An extended version is available as a Technical Report, Faculty of Information Systems and Applied Computer Sciences, Bamberg University, No. 101, June 2016.

2015

  • K. Rathlev, S. Smyth, Ch. Motika, R. von Hanxleden, M. Mendler: SCEst: Sequentially Constructive Esterel. In Proc. 13th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2015), Austin, Texas USA, September 21-23, 2015.
  • J. Aguado, M. Mendler, R. von Hanxleden, I. Fuhrmann: Denotational Fixed-Point Semantics for Constructive Scheduling of Synchronous Concurrency. In: Acta Informatica, Vol. 52(4), pp. 393-442, Springer, June 2015. DOI 10.1007/s00236-015-0238-x. A preliminary version is available as a Technical Report, Faculty of Information Systems and Applied Computer Sciences, Bamberg University, No. 96, April 2015.
  • R. von Hanxleden, B. Duderstadt, I. Fuhrmann, Ch. Motika, S. Smyth, M. Mendler, J. Aguado, S. Loftus-Mercer, O. O'Brien: Sequential Constructiveness and SCCharts for Safety-Critical Applications. In Software Engineering and Management 2015 (SE 2015), Dresden, March 2015, to appear in Springer LNI.

2014

  • M. Mendler, B. Bodin, P. S. Roop and J.-J. Wang: WCRT for synchronous programs - Studying the tick alignment problem.Technical Report,(2.4 MB) Faculty of Information Systems and Applied Computer Sciences, Bamberg University, No. 95, August 2014.
  • R. von Hanxleden, B. Duderstadt, Ch. Motika, S. Smyth, M. Mendler, J. Aguado, S. Mercer, O. O'Brien: SCCharts -Sequentially constructive statecharts for safety-critical applications. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI'14), Edinburgh, UK, June 2014.
  • R. von Hanxleden, M. Mendler, J. Aguado, et. al.: Sequentially constructive concurrency. A conservative extension of the synchronous model of computation. ACM Transactions on Embedded Computing Systems, Special Issue on Applications of Concurrency to System Design, 13(4s):144:1-144:26, July 2014.
  • J. Aguado, M. Mendler, Reinhard von Hanxleden, Insa Fuhrmann: Grounding Synchronous Deterministic Concurrency in Sequential Programming. In Z. Shao editor, European Symposium on Programming (ESOP 2014), Grenoble, France, Springer LNCS 8410, pp. 229-248. Extended version available as a Technical Report(1.1 MB), Faculty of Information Systems and Applied Computer Sciences, Bamberg University, No. 94, August 2014.
  • M. Mendler, S. Scheele: On the Computational Interpretation of CKn for Contextual Information Processing. Fundamenta Informaticae, Vol.130 (2014), pp.1-39. Proofs and ancillary Material.(524.3 KB)

2013

2012

  • M. Mendler, T. Shiple, G. Berry: Constructive Boolean circuits and the exactness of timed ternary simulation. Formal Methods in System Design, Vol.40, No.3, pp. 283-329, Springer. Online available as DOI 10.1007/s10703-012-0144-6.

2011

  • J. Aguado, M. Mendler, M. Pouzet: Unifying Synchronous Data and Control Flow in the Lazy Lambda Calculus. 23rd Nordic Workshop on Programming Theory (NWPT 2011), Vesteras, Sweden, October 2011.
  • J. Aguado, M. Mendler: An integrated data and control flow programming model. INForum 2011, Track CoRTA, Coimbra, Portugal, September 2011.
  • J. Aguado, M. Mendler: Computing with Streams. Declarative Aspects of Multicore Programming (DAMP 2011), Austin, Texas, 23 Jan 2011. 
  • J. Aguado, M. Mendler: Constructive Semantics for Instantaneous Reactions. Theoretical Computer Science, Vol. 421 (2011), pp. 931-961. 
  • M. Mendler and S. Scheele: Cut-free Gentzen Calculus for Multimodal CK. Journal of Information and Computation, Vol. 209 (2011), pp. 1465-1490.

2010

  • J. Aguado, M. Mendler: Towards Strategies for Dataflow Programming. 22nd Symposium on Implementation and Application of Functional Languages (IFL2010) . Alphen an den Rijn, Netherlands, 3rd September, 2010.
  • M. Mendler: An Algebra of Synchronous Scheduling Interfaces. Foundations of Interface Technologies (FIT 2010), Paris, 30th August 2010. 
  • M. Mendler and S. Scheele: Towards a Simply Typed CALculus for Semantic Knowledge. Logics for Agents and Mobility (LAM 2010), Edinburgh, July 2010.
  • W.-P. de Roever, G. Lüttgen, M. Mendler: What is in a Step: New Perspectives on a Classical Question. Z. Manna, D.A. Peled (eds.), Springer LNCS 6200, pp. 370-399.
  • M. Mendler, G. Luettgen: Is Observational Congruence on mu-Expressions Axiomatisable in Equational Horn Logic? Information and Computation, 208 (2010), pp. 634-651. 

2009

  • M. Mendler, S. Scheele: Towards Constructive DL for Abstraction and Refinement. Journal of Automated Reasoning, Vol. 44, No. 3, 2010, pp. 207-243. Online since 23.9.2009.
  • M. Mendler, S. Scheele: Exponential Speedup in UL Subsumption Checking Relative to General TBoxes for the Constructive Semantics. Proc. Int'l Workshop on Description Logic (DL 2009), Oxford, July 2009.
  • M. Mendler, S. Scheele: Towards a Type System for Semantic Streams. Stream Reasoning 2009. Heraklion, Crete, 31st May 2009. 
  • R. v. Hanxleden, M. Mendler, C. Traulsen: WCRT Algebra and Interfaces for Esterel-style Synchronous Processing. Design Automation and Test in Europe (DATE 2009), April 2009.
  • Aguado, J. & Macias, F. & Mendler, M. (2009) The Lusterel Library: Programming Combined Data and Control Flow Applications in Haskell. ACM SIGPLAN 2009 Developer Tracks on Functional Programming (DEFUN 2009) in conjunction with the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009). Edinburgh, Scotland, September 2009.

2008

  • F. Maraninchi, M. Mendler, M. Pouzet, A. Girault, E. Rutten: Selected Papers from SLA++P 07 and 08 Model-Driven High-Level Programming of Embedded Systems. EURASIP Journal of Embedded Systems, Vol. 2009, Hindawi Publishing Corporation, 2009.
  • M. Mendler: Lusterel - A Uniform and Modular Composition of Data-flow and Control-flow in Haskell
  • M. Mendler, S. Scheele: Constructive Description Logic cALC as a Type System for Semantic Streams in the Domain of Auditing. Logics for Agents and Mobility (LAM'08), Hamburg, August 2008.
  • M. Mendler, S. Scheele: Towards Constructive DL for Abstraction and Refinement. Int'l Workshop on Description Logic (DL 2008), Dresden, May 2008. 
  • J. Aguado, M. Mendler, (eds.): Proceedings Model-driven High-level Programming of Embedded Systems (SLA++P 2007). Electronic Notes in Theoretical Computer Science, Issue 4, Vol 203. Elsevier, June 2008.

2007

  • M. Mendler, G. Lüttgen: Is Observational Congruence Axiomatisable in Equational Horn Logic? In L. Caires and V. T. Vasconcelos (eds.) Proc. Int'l Conference on Concurrency Theory (CONCUR 2007), Lisbon, Portugal, September 2007. Springer LNCS 4703, pp. 197--211.
  • M. Mendler, G. Lüttgen: Is Observational Congruence on mu-Expressions Axiomatisable in Equational Horn Logic? Technical Report 72/2007, The University of Bamberg, Fakultät für Wirtschaftsinformatik und Angewandte Informatik, June 2007, (57 pages).

2006

  • M. Mendler, T. R. Shiple, G. Berry: Constructive Circuits and the Exactness of Ternary Simulation. Technical Report 68/2006, The University of Bamberg, Fakultät für Wirtschaftsinformatik und Angewandte Informatik, September 2006 (83 pages).
  • M. Mendler: The Synchrony Hypothesis or the Importance of Being Constructive. Synchron 2006, L'Alpe D'Huez, France, 30th November 2006. (pdf(738.8 KB))

2005

  • M. Mendler: Propositional Stabilisation Theory. Interface Types for Causality and Timing Analysis. Synchron 2005, Qwara, Malta, 21.-25. November 2005. (pdf(1.9 MB))
  • J. Aguado, M. Mendler: Towards Unit Testing for Communicating Stream X-machines Systems. In R. Hierons, P. McMinn (eds.), UK Software Testing Research III (UKTest 2005), University of Sheffield, Department of Computer Science, September 5-6, 2005, pp. 39-66.
  • J. Aguado, M. Mendler: Constructive Game Semantics for Instantaneous Reactions. In: D. R. Ghica and G. McCusker (eds.) Games for Logics and Programming Languages (GaLoP 2005), Edinburgh, April 2005, pp. 16-31. (updated version(635.2 KB)). Extended version available as Technical Report 63/2005, The University of Bamberg, Fakultät für Wirtschaftsinformatik und Angewandte Informatik, February 2005 (48 pages).
  • G. Lüttgen, M. Mendler: When 1 Clock is Not Enough. In: L. Aceto and A.D. Gordon (eds.), Algebraic Process Calculi: The First Twenty Five Years and Beyond (PA'05), Bertinoro, University of Bologna, August 1-5, BRICS Notes Series, NS-05-03, June 2005, pp.155-158.
  • M. Mendler, V. De Paiva: Constructive CK for Contexts. In L. Serafini, P. Bouquet (eds.), Proceedings Context Representation and Reasoning (CRR-2005), Paris, July 2005, Vol. 136 of CEUR Proceedings (pdf(576.3 KB)). Also presented at the Association for Symbolic Logic Annual Meeting, Stanford University, USA, 22nd March 2005.
  • G. Lüttgen, N. Martinez Madrid, M. Mendler (eds.): Proceedings Workshop Semantic Foundations of Engineering Design Languages (SFEDL 2004), Electronic Notes in Theoretical Computer Science, Elsevier, Vol. 115, January 2005.

2004

  • V. De Paiva, R. Gore, M. Mendler (eds.): Modalities in Constructive Modal Logics and Type Theories. Special issue of the Journal Logic and Computation, editorial pp. 439-446, Vol. 14, No. 4, Oxford University Press, August 2004.
  • M. Broy, G. Lüttgen, M. Mendler (eds.): Semantic Foundations of Engineering Design Languages. Special issue of the Journal Formal Aspects of Computing, Vol. 16, No. 4, August 2004, Springer Verlag.

2003

  • J. Aguado, G. Luettgen, M. Mendler: A-maze-ing Esterel. In F. Maraninchi, A. Girault, E. Rutten (eds.), Synchronous Languages, Applications, and Programming (SLAP'03), Porto, July 2003, Electronic Notes in Theoretical Computer Science, to appear. pdf(837.9 KB) (draft version).
  • M. Broy, G. Lüttgen, M. Mendler (eds.): Semantic Foundations of Engineering Design Languages (Part I), International Journal on Formal Aspects of Computing, Vol. 15, No. 4, December 2003, Springer Verlag.
  • B. Norton, G. Luettgen, M. Mendler: A compositional semantic theory for synchronous component-based design. In R. Amadio, D. Lugiez (eds.), Int'l Conference on Concurrency Theory (CONCUR'03), Springer LNCS 2761, 2003, pp. 461-476. pdf(676.2 KB) (draft)
  • M. Fairtlough, M. Mendler: Intensional completeness in an extension of Goedel-Dummett Logic. Studia Logica, Vol.73, January, 2003, pp. 51-80. abstract, pdf(1.4 MB).

2002

  • J. Aguado and A.J. Cowling: Design Models and the Complexity of the Testing Problem for Distributed Systems. International Workshop on Semantic Foundations of Engineering Design Languages (SFEDL'02), Grenoble, France, April, 2002.
  • J. Aguado and A.J. Cowling: Foundations of the X-machine Theory for Testing. Research Report CS-02-06. Department of Computer Science, University of Sheffield, 2002.
  • J. Aguado and A.J. Cowling: Systems of Communicating X-machines for Specifying Distributed Systems. Research Report CS-02-07. Department of Computer Science, University of Sheffield, 2002.
  • G. Luettgen, M. Mendler: Axiomatizing an Algebra of Step Reactions for Synchronous Languages. In L. Brim, P. Jancar, M. Ketinsky, A. Kucera (eds.), Int'l Conference on Concurrency Theory (CONCUR'02), Springer LNCS 2421, 2002, pp. 386-401. pdf(1.1 MB)
  • G. Luettgen, M. Mendler: Towards a Model Theory for Esterel. In F. Maraninchi, A. Girault, E. Rutten (eds.), Synchronous Languages and Applications (SLAP'02), Electronic Notes in Theoretical Computer Science, Vol. 65, No. 5, April 2002. pdf(1.3 MB).
  • M. Fairtlough, M. Mendler: On the Logical Content of Computational Type Theory: A Solution to Curry's Problem. In P. Callaghan, Z. Luo, J. McKinna (eds.), Types for Proofs and Programs, Springer 2002 (LNCS 2277), pp. 63-78. abstract, pdf(598.8 KB).
  • G. Luettgen, M. Mendler: The Intuitionism behind Statecharts Steps. ACM Transactions on Computational Logic, Vol. 3, No. 1, pp. 1-41, 2002.

2001

  • G. Luettgen, M. Mendler: Statecharts: From visual syntax to model-theoretic semantics. Workshop on Integrating Diagrammatic and Formal Specification Techniques. In K. Bauknecht, W. Brauer, Th. Mueck (eds.), Informatik 2001: Wirtschaft und Wissenschaft in der Network Economy - Visionen und Wirklichkeit, Vol. 1, Vienna, Austrian Computer Society, September 2001, pp. 615-621. pdf(1.2 MB)
  • M. Fairtlough, M. Mendler, X. Cheng: Abstraction and refinement in higher-order logic. In R. J. Boulton, P. B. Jackson (eds), Theorem-proving in Higher-order Logic (TPHOLs'2001), pp. 201-216, Springer LNCS 2152, 2001. abstract, pdf(1.1 MB).
  • N. Alechina, M. Mendler, V. de Paiva, E. Ritter: Categorical and Kripke semantics for constructive modal logics. In L. Fribourg (ed.), Computer Science Logic (CSL'01), pp. 292-307, Springer LNCS 2142, 2001. abstract, pdf(617.5 KB).
  • M. Fairtlough, M. Mendler, E. Moggi (eds.): Modalities in Type Theory. Mathematical Structures in Computer Science, Vol. 11, No. 4, August 2001.
  • X. Cheng, M. Fairtlough, M. Mendler: Proofs as Constraints for Abstraction and Refinement. In U. Egly, A. Fiedler, H. Horacek, S. Schmitt (eds.), Proc. Workshop on Proof Transformations, Proof Presentations and Complexities of Proof (PTP'01). pp.1-11, University of Siena, June 2001.

2000

  • G. Luettgen, M. Mendler: Fully-abstract Statecharts semantics via intuitionistic Kripke models. In U. Montanari, J. Rolim, E. Welzl (eds.), Proc. 27th Int'l Colloquium on Automata, Languages and Programming (ICALP'00), pp.163-174, Springer 2000 (LNCS 1853). abstract, bibtex(575.0 B), pdf(818.8 KB).
  • G. Luettgen, M. Mendler: What is in a Step: A Fully-abstract semantics for Statecharts macro steps via intuitionistic Kripke models. University of Sheffield, Department of Computer Science, Technical Report CS-00-04, 48 pages. pdf(505.7 KB)
  • G. Lüttgen, M. Mendler: The intuitionism behind Statecharts steps. Technical Report, NASA Langley Research Center, Institute for Computer Computer Applications in Science and Engineering ICASE CR-2000-210302, 40 pages.
  • M. Mendler: Characterising Timing Analyses in Intuitionistic Modal Logic. Logic Journal of the IGPL, Vol 8, No. 6, pp. 821-853, 2000. pdf(799.7 KB), abstract.
  • M. Mendler: Timing analysis of combinational circuits in intuitionistic propositional logic. Formal Methods in System Design, Vol. 17, Nr. 1, pp. 5-37, 2000. abstract, bibtex(478.0 B), pdf(1.5 MB).

1999

  • T. Lock, M. Mendler: Äquivalenz von annotierten Kontrollflußgraphen zur Darstellung von HLS-Ein- und -Ausgaben bei Verwendung pfadbasierter Einplanungsverfahren. In M. Mutz, N. Lange (eds.), GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", pp.51-60, Braunschweig, Shaker, 1999.

1998

  • A. Sicheneder, A. Bender, E. Fuchs, M. Mendler, B. Sick: Tool-supported Software Design and Program Execution for Signal Processing Appliations Using Modular Software Components. In T. Margaria, B. Steffen (eds.), Proc. International Workshop on Software Tools for Technology Transfer (STTT'98), pp. 61-70, 1998.
  • T. Margaria, M. Mendler, C. Gsottberger: Modelling and Verification of Unbounded Length Systolic Arrays in Monadic Second-Order Logic. Int. Workshop on Infinite State Systems (Infinity'98), pp 99-112, TU München, 1998.
  • Th. Lock, M. Mendler, M. Mutz: Combined Formal Post- and Presynthesis Verification in High Level Synthesis. In G. Gopalakrishnan and Ph. Windley (eds.), Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD'98), pp. 222-236, Springer 1998 (LNCS 1522).
  • Th. Lock, M. Mendler: Formale Modellierung von kontrollflußdominierten High-Level-Synthese-Eingabebeschreibungen zur Verifikation von Ergebnissen kontrollflußgesteuerter Einplanungsverfahren. In F. J. Rammig, W. Müller (eds.), Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, pp. 75-84, HNI Verlagsschriftenreihe, March 1998.
  • M. Mendler: Characterising timing analyses in intuitionistic modal logic. In R. J. DeQueiroz, M. Finger (eds.), Workshop on Logic, Language and Computation (WOLLIC'98), pp. 132-140, University of Sao Paulo, Brazil, 1998.

1997

  • M. Fairtlough, M. Mendler: Propositional Lax Logic. Information and Computation, Vol.137, No.1, 1997, pp. 1-33. abstract, bibtex(288.0 B), pdf(1.1 MB).
  • M. Fairtlough, M. Mendler, M. Walton: First-order Lax Logic as a framework for Constraint Logic Programming. Technical Report MIP 9714, Passau University, 1997, 51 pages. abstract, pdf(662.5 KB).
  • P. Kelb, T. Margaria, M. Mendler, C. Gsottberger: MOSEL: A flexible toolset for monadic second-order logic. In E. Brinksma (ed.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97), pp 183-202, Springer 1997 (LNCS 1217). abstract, bibtex, pdf.
  • P. Kelb, T. Margaria, M. Mendler, C. Gsottberger: Mosel: A Sound and Efficient Tool for M2L(Str).
    In O. Grumberg (ed.), Computer-Aided Verification (CAV'97), pp. 448-451, Springer 1997 (LNCS 1254).
    T. Margaria and M. Mendler: Model-based Automatic Synthesis and Analysis in Second-Order Monadic Logic. In R. Cleaveland, D. Jackson (eds.), Proc. ACM SIGPLAN Workshop on Automated Analysis of Software (AAS'97), pp. 99-112, Paris, ACM, January 1997.
  • R. Cleaveland, G. Luettgen, M. Mendler: An algebraic theory of multiple clocks. In Proc. of the International Conference on Concurrency Theory (CONCUR'97), pp. 166-180, Springer 1997 (LNCS 1243). abstract, bibtex(429.0 B), pdf(577.4 KB).

1996

  • M. Mendler, M. Fairtlough: Ternary simulation: Refinement of binary functions or abstraction of real-time behaviour? In M. Sheeran and S. Singh (eds.), Proc. Workshop on Designing Correct Circuits (DCC'96), Springer Electronic Workshops in Computing, October 1996, 17 pages. abstract, bibtex(433.0 B), pdf(856.7 KB).
  • M. Mendler: Timing Refinement of Intuitionistic Proofs and its Application to the Timing Analysis of Combinational Circuits. In P. Miglioli, U. Moscato, D. Mundici, M. Ornaghi (eds.), Proc. International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'96), pp. 261-277, Springer 1996 (LNAI 1071).
  • M. Mendler: Timing refinement of intuitionistic proofs. In: B. Straube (ed.), GI/ITG/GME Workshop Methoden des Entwurfs und der Verifikation Digitaler Systeme, pp. 121-130, Shaker, 1996.
    T. Margaria, M. Mendler: Automatic treatment of sequential circuits in second-order monadic logic. In: B. Straube (ed.), GI/ITG/GME Workshop Methoden des Entwurfs und der Verifikation Digitaler Systeme, pp. 21-30, Shaker, 1996.

1995

  • H. R. Andersen, M. Mendler: Describing a signal analyzer in the process algebra PMC -- A case study. In P. D. Mosses, M. Nielsen, M. Schwartzbach (eds.), Theory and Practice of Software Development (TAPSOFT'95), pp.620-635, Springer 1995 (LNCS 915). abstract, bibtex(396.0 B), pdf(860.9 KB).
  • M. Fuchs, M. Mendler: Functional Semantics for Delta-VHDL based on FOCUS. In C. D. Kloos and P. T. Breuer (eds.), Formal Semantics for VHDL, Chap. 1, Kluwer 1995.
  • L. G. Wang, M. Mendler: The formal design of a class of computers - Its high stage: abstract microprogramming. In H. Eveking and P. Camurati (eds.), Proc. Correct Hardware Design and Verification Methods (CHARME'95), pp. 84-102, Springer 1995 (LNCS 987).
  • L. G. Wang, M. Mendler: Abstraction of Hardware Construction. In G. Dowek, J. Heering, B. Möller, K. Meinke (eds.), Proc. Higher-Order Algebra, Logic, and Term Rewriting, (HOA'95), pp. 264-287, Springer 1995 (LNCS 1074).
  • M. Fairtlough, M. Mendler: An intuitionistic modal logic with applications to the formal verification of hardware. In L. Pacholski and J. Tiuryn (eds.), Proc. of the 1994 Annual Conference of the European Association for Computer Science Logic (CSL'94), pp. 354-368, Springer 1995 (LNCS 933).
  • M. Mendler: Can we specify finite-state systems in a fragment of propositional logic? In: B. Straube (ed.) Use of Process Algebras in Design (3rd Euroform Workshop), Dresden, February 1995, 23 pages.

1994

  • H. R. Andersen, M. Mendler: An asynchronous process algebra with multiple clocks. In D. Sannella (ed.), Proc. European Symposium on Programming (ESOP'94), pp. 58-73, Springer 1994 (LNCS 788).
  • M. Mendler: Dealing with hardware constraints - a modal logical approach. In: C. D. Kloos (ed.) 1st Euroform Workshop, Las Navas del Marques, Spain, January 1994, 7 pages.

1993

  • H. R. Andersen, M. Mendler: An process algebra with multiple clocks. Technical report, Technical University of Denmark ID-TR:1993-122, 40 pages.
  • M. Mendler, T. Stroup: Newtonian arbiters cannot be proven correct. Formal Methods in System Design, Vol.3, No.3, 1993, pp. 233-257. abstract, bibtex(306.0 B).
  • M. Mendler: A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD Thesis, Department of Computer Science, University of Edinburgh, March 1993, ECS-LFCS-93-255.
  • H. R. Anderen, M. Mendler: A complete axiomatization of observation congruence in PMC. Technical report, Technical University of Denmark ID-TR:1993-126, 25 pages.

1992

  • B. Steffen, C. B. Jay, M. Mendler: Compositional characterization of observable program properties. Theoretical Informatics and Applications, Vol.26, No.5, pp. 403-424, 1992.
  • T. Reinhardt, M. Mendler, T. Stroup: Die formale Validierung einer Bausteintafel delay-insensitiver Grundelemente. In M. Glesner (editor) ITG/GME/GI Fachtagung Rechnergestützter Entwurf und Architektur Mikroelektronischer Systeme, pp. 273-274, VDE Verlag, 1992.

1991

  • M. Mendler: Constrained proofs: a logic for dealing with behavioural constraints in formal hardware verification. In G. Jones and M. Sheeran (eds.), Proc. Workshop on Designing Correct Circuits (DCC'91), pp.1-28, Springer 1991.

1989

  • T. Stroup, N. Götz, M. Mendler: Stepwise refinement of layered protocols by formal program development. In E. Brinksma, G. Scollo, Ch. A. Visser (eds.), 9th IFIP WG6.1 Int'l Symposium on Protocol Specification, Testing, and Verification, 14 pages, 1989.