Veröffentlichungen der Arbeitsgruppe

      2023
 

  • David Boetius, Stefan Leue, and Tobias Sutter. 2023. A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks. CoRR abs/2301.11342. Accepted at ICML 2023. [ICML 2023] [PDF]
  • David Boetius, Stefan Leue. 2023. Verifying Global Neural Network Specifications using Hyperproperties. CoRR abs/2306.12495. Accepted at FoMLAS 2023. [FoMLAS 2023] [PDF]
  • F. Bauer-Marquart, S. Leue, and C. Schilling. 2023. symQV: Automated Symbolic Verification of Quantum Programs. In FM - 25th International Symposium on Formal Methods, Lecture Notes in Computer Science, vol. 14000, Springer Verlag, 181-198. [PDF] [FM 2023] [arXiv]
  • A. Khoja, M. Kölbl, S. Leue, and R. Wilhelmi. 2023. Formal Modeling and Analysis of Legal Contracts using ContractCheck. Presented at the Workshop on Programming Languages and the Law, ProLaLa 2023. [arXiv] [PDF] [ProLaLa 2023]

      2022
 

  • Fabian Bauer-Marquart, David Boetius, Stefan Leue, Christian Schilling. 2022. SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks. In SPIN 2022, 79-96. [SPIN 2022] [PDF]
  • M. Kölbl, S. Leue, and T. Wies. 2022. Automated Repair for Timed Systems. In Formal Methods in System Design, Springer Verlag. Accepted for publication. [Journal] [PDF Pre-Version]
  • M. Kölbl, A. Khoja, S. Leue, and R. Wilhelmi. 2022. Automated Consistency Analysis for Legal Contracts. In Proceedings of the 28th International SPIN Symposium on Model Checking of Software, Lecture Notes in Computer Science, vol. 13255, Springer Verlag, 1-23. [SPIN 2022] [PDF]
  • G. Caltais, H. Hojjat, M. R. Mousavi, and H. C. Tunc. 2022. DyNetKAT: An Algebra of Dynamic Networks. In FoSSaCS - 25th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 13242, Springer Verlag, 184-204. [FoSSaCS 2022] [PDF]

      2021
 

  • G. Caltais and H. C. Tunc. 2021. Explaining Safety Failures in NetKAT. In Journal of Logical and Algebraic Methods in Programming, Elsevier. [Journal] [PDF]
  • M. Kölbl and S. Leue. 2020. An Algorithm to Compute a Strict Partial Ordering of Actions in Action Traces. In ISOLA - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. [ISoLA 2020] [PDF]

      2020
 

  • M. Kölbl, S. Leue, and R. Schmid. 2020. Dynamic Causes for the Violation of Timed Reachability Properties. In FORMATS - 18th International Conference on Formal Modeling and Analysis of Timed Systems, Lecture Notes in Computer Science, vol. 12288, pp. 127-143, Springer Verlag. [FORMATS 2020] [PDF]
  • G. Caltais, M. R. Mousavi, and H. Singh. 2020. Causal Reasoning for Safety in Hennessy Milner Logic. In Fundamneta Informaticae, vol. 173, no. 2-3, pp. 217–25, IOS Press. [Journal] [PDF]
  • M. Kölbl, S. Leue, and T. Wies. 2020. TarTar: A Timed Automata Repair Tool. In CAV(1) - 32th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 12224, pp. 529-540, Springer Verlag. Long Version: CoRR abs/2002.02760. [PDF] [CAV 2020]
  • G. Caltais, S. Leue, and H. Singh. 2020. Correctness of an ATL Model Transformation from SysML State Machine Diagrams to Promela. In MODELSWARD - 8th International Conference on Model-Driven Engineering and Software Development, pp. 360 - 372, Scitepress. [PDF] [MODELSWARD 2020]

 

      2019
 

  • M. Kölbl, S. Leue, and T. Wies. 2019. Clock Bound Repair for Timed Systems. In CAV (1) - 31st International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, vol. 11561, pp. 79-96, Springer Verlag. [CAV 2019] [PDF]
  • M. Kölbl and S. Leue. 2019. An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking. In ATVA - 17th International Symposium on Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, vol. 11781, pp. 171-186, Springer Verlag. [ATVA 2019] [PDF]
  • G. Caltais. 2019. Explaining SDN Failures via Axiomatisations. In FROM - Proceedings 3rd Symposium on Working Formal Methods, vol. 303, pp. 48-60. [arXiv 2019] [PDF]
  • G. Gössler, S. Leue, and S. Nakajima. 2019. Causal Reasoning in Systems. Technical Report, NII Shonan Meeting Report. [NII 2019] [PDF]

      2018

  • M. Kölbl and S. Leue. 2018. Automated Functional Safety Analysis of Automated Driving Systems. In Formal Methods for Industrial Critical Systems, Proceedings of the 23rd International FMICS Conference, Maynooth, Ireland. Lecture Notes in Computer Science, Volume 11119, pp 35-51, Springer Verlag. [FMICS 2018] [PDF]
  • M. Kölbl, S. Leue, and H. Singh. 2018. From SysML to Model Checkers via Model Transformation. Proceedings of the 25th International SPIN Symposium on Model Checking of Software. [SPIN 2018] [PDF]
  • G. Caltais, S. L. Guetlein, and S. Leue. 2018. Causality for General LTL-definable Properties. 3rd Workshop on Formal Reasoning about Causation, Responsibility and Explanations in Science and Technology. [arXiv 2018] [PDF]
  • G. Caltais and M. R. Mousavi. 2018. Encoding Causality via Modal Formulae. Working Formal Methods Symposium. [PDF]

     2017
 

  • A. Groce and S. Leue. 2017. Proceedings of the 2nd International Workshop on Causal Reasoning for Embedded and Safety-critical Systems Technologies, CREST@ETAPS. [arXiv]

     2016
 

  • G. Caltais, S. Leue, and M. R. Mousavi. 2016. (De-)Composing Causality in Labeled Transition Systems. In CREST: 1st Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies. [arXiv 2016] [PDF]
  • G. Caltais, F. Leitner-Fischer, S. Leue, and J. Weiser. 2016. SysML to NuSMV Model Transformation via Object-Orientation. In Sixth Workshop on Design, Modeling and Evaluation of Cyber Physical Systems. [CyPhy 2016] [PDF]
  • G. Caltais, S. Leue, and M. R. Mousavi. 2016. On (De-)Composing Causality. In 28th Nordic Workshop on Programming Theory. [PDF]
  • G. Caltais and B. Meyer. 2016. On the Verification of SCOOP Programs. In Science of Computer Programming. [Journal] [PDF]
  • F. Leitner-Fischer, S. Leue, and S. Liu. 2016. Automated Freedom from Interference Analysis for Automotive Software. In Proceedings of 4th International Workshop on Critical Automotive Applications: Robustness & Safety (CARS 2016), Gothenburg, Sweden. [CARS 2016][PDF]

2015
 

  • Florian Leitner-Fischer. 2015. Causality Checking of Safety-Critical Software and Systems. Ph.D. Dissertation. University of Konstanz. [PDF]
  • A. Bey and C. Wienbruch. 2015. Intrinsic Network Properties Govern the Network Response to Repetitive Transcranial Magnetic Stimulation (rTMS) in a Neuronal Network Model Simulating the Effects of rTMS. In Clinical Neurophysiology. 126 (8), e125-e126. [Journal] [PDF]
  • A. Beer, S. Heidinger, U. Kühne, F. Leitner-Fischer, and S. Leue. 2015. Symbolic Causality Checking Using Bounded Model Checking. International SPIN Workshop on Model Checking of Software. volume 9232. pp 203-221. [SPIN 2015] [PDF]

2014

  • Florian Leitner-Fischer and Stefan Leue. 2014. SpinCause: A Tool for Causality Checking. In Proceedings of the International SPIN Symposium on Model Checking of Software, San Jose, CA, USA. [SPIN 2014] [­PDF]
  • Adrian Beer, Florian Leitner-Fischer and Stefan Leue. 2014. On the Relationship of Event Order Logic and Linear Temporal Logic. Technical Report soft-14-01, Chair for Software Engineering, University of Konstanz. [PDF]
  • Adrian Beer, Uwe Kühne, Florian Leitner-Fischer and Stefan Leue. 2014. Towards Symbolic Causality Checking using SAT-Solving. In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2014), Dagstuhl, Germany. [PDF]
  • A. Beer, U. Kühne, F. Leitner-Fischer, S. Leue, and R. Prem. 2014. Symbolic Causality Checking Using SAT-Solving. Technical Report soft-14-02, Chair for Software Engineering, University of Konstanz. [PDF]

2013

  • F. Leitner-Fischer and S. Leue. 2013. Probabilistic Fault Tree Synthesis using Causality Computation. In International Journal of Critical Computer-Based Systems, Vol. 4, No. 2, pp.119–143. [Journal] [PDF]
  • F. Leitner-Fischer and S. Leue. 2013. Probabilistic Fault Tree Synthesis using Causality Computation. Technical Report soft-13-03, Chair for Software Engineering, University of Konstanz. [PDF]
  • F. Leitner-Fischer and S. Leue. 2013. On the Synergy of Probabilistic Causality Computation and Causality Checking. In Model Checking Software - Proceedings of International SPIN Symposium on Model Checking of Software. Stony Brook, NY, USA. LNCS Volume 7976, pp 246-263, Springer Verlag. [SPIN 2013] [PDF]
  • S. Leue and M. Tabaei Befrouei. 2013. Mining Sequential Patterns to Explain Concurrent Counterexamples. In Model Checking Software - Proceedings of International SPIN Symposium on Model Checking of Software. Stony Brook, NY, USA. LNCS Volume 7976, pp 264-281, Springer Verlag.  [SPIN 2013] [PDF]
  • A. Beer, T. Georgiev, F. Leitner-Fischer, and S. Leue. 2013. Model-Based Quantitative Safety Analysis of Matlab Simulink / Stateflow Models. In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2013). Dagstuhl, Germany. [PDF]
  • A. Beer, U. Kühne, F. Leitner-Fischer, S. Leue, and R. Prem. 2013. Quantitative Safety Analysis of Non-Deterministic System Architectures. Technical Report soft-13-02, Chair for Software Engineering, University of Konstanz. [PDF]
  • F. Leitner-Fischer and S. Leue. 2013. On the Synergy of Probabilistic Causality Computation and Causality Checking. Technical Report soft-13-01, Chair for Software Engineering, University of Konstanz. [SPIN 2013] [PDF]
  • F. Leitner-Fischer and S. Leue. 2013. Causality Checking for Complex System Models. In Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation ,pp. 248-267, LNCS, Volume 7737. Springer Verlag. [VMCAI 2013] [PDF]

2012

  • A. Bey, S. Leue, and C. Wienbruch. 2012. A Neuronal Network Model for Simulating the Effects of Repetitive Transcranial Magnetic Stimulation on Local Field Potential Power Spectra. In PLOS ONE, 7(11): e49097. [Journal] [PDF]
  • A. Beer. 2012. Quantitative Analysis of Concurrent System Architectures. Master Thesis, University of Konstanz. [PDF]
  • S. Leue and M. Tabaei Befrouei. 2012. Counterexample Explanation by Anomaly Detection. In Proceedings of 19th International SPIN Workshop on Model Checking of Software. LNCS, Volume 7385, pp. 24-42. Springer Verlag. [SPIN 2012] [PDF]
  • F. Leitner-Fischer and S. Leue. 2012. Causality Checking for Complex System Models. Technical Report soft-12-02, Chair for Software Engineering, University of Konstanz. [PDF]
  • A. Beer, U. Kühne, F. Leitner-Fischer, S. Leue, and R. Prem. 2012. Analysis of an Airport Surveillance Radar using the QuantUM approach. Technical Report soft-12-01, Chair for Software Engineering, University of Konstanz. [PDF]
  • F. Leitner-Fischer and S. Leue. 2012. Towards Causality Checking for Complex System Models. In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme (MBEES 2012). Dagstuhl, Germany. [PDF]

2011

  • H. Aljazzar and S. Leue. 2011. K*: A Heuristic Search Algorithm for Finding the k Shortest Paths. Artificial Intelligence, 175(18). [AI 2011] [PDF]
  • M. Kuntz, F. Leitner-Fischer, and S. Leue. 2011. From Probabilistic Counterexamples via Causality to Fault Trees. In Proceedings of 30th International Conference on Computer Safety, Reliability and Security. [SAFECOMP 2011] [PDF]
  • H. Aljazzar, F. Leitner-Fischer, S. Leue, and D. Simeonov. 2011. DiPro - A Tool for Probabilistic Counterexample Generation. In Proceedings of 18th International SPIN Workshop on Model Checking of Software. [SPIN 2011] [PDF]
  • D. Lehle. 2011. Quantitative Safety Analysis of SysML Models. Bachelor Thesis, University of Konstanz. [PDF]
  • A. Bey and S. Leue. 2011. Modeling and Analyzing Spike Timing Dependent Plasticity with Linear Hybrid Automata. Technical Report soft-11-03, Chair for Software Engineering, University of Konstanz. [PDF]
  • M. Kuntz, F. Leitner-Fischer, and S. Leue. 2011. From Probabilistic Counterexamples via Causality to Fault Trees. Technical Report soft-11-02, Chair for Software Engineering, University of Konstanz. [PDF]
  • F. Leitner-Fischer and S. Leue. 2011. The QuantUM Approach in the Context of the ISO Standard 26262 for Automotive Systems. Technical Report soft-11-01, Chair for Software Engineering, University of Konstanz. [PDF]
  • M. Kuntz, F. Leitner-Fischer, S. Leue, and B. Reh. 2011. Challenges in the Modelling and Quantitative Analysis of Safety-Critical Automotive Systems. Presentation at ROCKS workshop (ROCKS 2011). Saarbrücken, Germany. [PDF]
  • F. Leitner-Fischer and S. Leue. 2011. QuantUM: Quantitative Safety Analysis of UML Models. In Proceedings of Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011). Saarbrücken, Germany. [QAPL 2011] [PDF]
  • F. Leitner-Fischer and S. Leue. 2011. Quantitative Analysis of UML Models. In Proceedings of Modellbasierte Entwicklung eingebetteter Systeme. Dagstuhl, Germany. [PDF]
  • S. Leue and W. Wei. 2011. Integer Linear Programming Based Property Checking for Asynchronous Reactive Systems. IEEE Transactions on Software Engineering, vol. 99. [Journal] [PDF]

2010

  • F. Leitner-Fischer. 2010. Quantitative Safety Analysis of UML Models. Master Thesis, University of Konstanz. [PDF]
  • B. R. Haverkort, M. Kuntz, F. Leitner-Fischer, A. Remke, and S. Roolvink. 2010. Probabilistic verification of Architectural software models using SoftArc and Prism. In Proceedings of the ESREL 2010 Annual Conference (ESREL '10), 5-9 Sept. Rhodos, Greece. Taylor & Francis. pp. 852-860. [PDF]
  • B.R. Haverkort, M. Kuntz, A. Remke, and S. Roolvink. 2010. Formal Performability Evaluation of Architectural Models of Critical Infrastructures. In Proceedings of the ESREL 2010 Annual Conference (ESREL '10), 5-9 Sept. Rhodos, Greece. Taylor & Francis Group. pp. 27-34. [PDF]
  • B.R. Haverkort, M. Kuntz, A. Remke, S. Roolvink, and M.I.A. Stoelinga. Evaluating Repair Strategies for a Water-Treatment Facility using Arcade. In 2010 IEEE/IFIP International Conference on Dependable Systems & Networks (DSN '10), 28 June - 1 July. Chicago, IL, USA. IEEE Computer Society Press. pp. 419-424. [DSN 2010] [PDF]
  • M. Kuntz, S. Leue, and C. Scheben. 2010. Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs. In Third International Workshop on Invariant Generation. [WING 2010] [PDF]
  • H. Aljazzar and S. Leue. 2010. K*: Heuristics-Guided, On-the-Fly k Shortest Paths Search. In Sixth Workshop on Model Checking and Artificial Intelligence (MoChArt '10). [PDF]
  • H. Aljazzar, M. Kuntz, F. Leitner-Fischer, and S. Leue. 2010. Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation. In Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems. [ICSE 2010] [PDF]

2009

  • H. Aljazzar. 2009. Directed Diagnostics of System Dependability Models. Doctoral Dissertation, University of Konstanz. [PDF]
  • M. Kuntz, S. Leue, C. Scheben, W. Wei, and S. Yang. 2009. Heuristic Search for Unbounded Executions. Technical Report soft-09-02, Chair for Software Engineering, University of Konstanz. [PDF]
  • H. Aljazzar and S. Leue. 2009. Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking. IEEE Transactions on Software Engineering. IEEE Computer Society. [IEEE 2009] [PDF]
  • B. Badban, S. Leue, and J.-G. Smaus. 2009. Automated Predicate Abstraction for Real-Time Models. INFINITY 2009, 11th International Workshop on Verification of Infinite-State Systems. [INFINITY 2009] [PDF]
  • B. Badban, S. Leue, and J.-G. Smaus. 2009. Automated Invariant Generation for the Verification of Real-Time Systems. International Workshop on Invariant Generation. [WING 2009] [PDF]
  • B. Badban. 2009. A Term Rewriting Technique for Decision Graphs. International Workshop on Computing with Terms and Graphs. [TERMGRAPH 2009] [PDF]
  • S. Edelkamp, V. Schuppan, D. Bosnacki, A. Wijs, A. Fehnker, and H. Aljazzar. 2009. Survey on Directed Model Checking. Model Checking and Artificial Intelligence, 5th International Workshop, MoChArt '08. Revised Selected and Invited Papers, Lecture Notes in Computer Science, Springer Verlag. Volume 5348, pp. 65-89. [MoChArt 2008] [PDF]
  • H. Aljazzar and S. Leue. 2009. Generation of Counterexamples for Model Checking of Markov Decision Processes. Proceedings of 6th International Conference on the Quantitative Evaluation of SysTems. IEEE Computer Society Press. [QEST 2009] [PDF]
  • H. Aljazzar, M. Fischer, L. Grunske, M. Kuntz, F. Leitner-Fischer, and S. Leue. 2009. Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples. Proceedings of 6th International Conference on the Quantitative Evaluation of SysTems (QEST '09). IEEE Computer Society Press. [QEST 2009] [PDF]
  • C. Dax, F. Klaedtke, and S. Leue. 2009. Specification Languages for Stutter-Invariant Regular Properties. Automated Technology for Verification and Analysis, 7th International Symposium, Lecture Notes in Computer Science, Springer Verlag. [ATVA 2009] [PDF]
  • H. Aljazzar, M. Fischer, L. Grunske, M. Kuntz, F. Leitner-Fischer, and S. Leue. 2009. Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples. Technical Report soft-09-01, Chair for Software Engineering, University of Konstanz. [PDF]
  • D. Bosnacki, S. Leue, and A. Lluch Lafuente. 2009. Partial-order reduction for general state exploring algorithms. International Journal on Software Tools for Technology Transfer (STTT). Springer Berlin / Heidelberg. Volume 11, pp. 39-51. [STTT 2009] [PDF]

2008

  • F. Leitner and S. Leue. 2008. Simulink Design Verifier vs. SPIN - A Comparative Case Study. Participant's Proceedings of FMICS 2008, ERCIM Working Group on Formal Methods for Industrial Critical Systems. [PDF]
  • B. Badhan. 2008. Prove with GDPLL-WD. A Complete Proof Procedure for Recursive Data Structures. Technical Report soft-08-07, Chair for Software Engineering, University of Konstanz. [PDF]
  • B. Badban. 2008. Culling predicates for the Verification of Real-Time Models. Technical Report soft-08-06, Chair for Software Engineering, University of Konstanz. [PDF]
  • F. Leitner. 2008. Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN. Technical Report soft-08-05, Chair for Software Engineering, University of Konstanz. [PDF]
  • B. Badban, W. Fokkink, and J. van de Pol. 2008. Mechanical Verification of a Two-Way Sliding Window Protocol. Communicating Process Architectures (CPA) conference. [CPA 2008] [PDF]
  • H. Aljazzar and S. Leue. 2008. Debugging of Dependability Models Using Interactive Visualization of Counterexamples. Proceedings of 5th International Conference on the Quantitative Evaluation of SysTems (QEST), IEEE Computer Society Press. [QEST 2008]
  • H. Aljazzar and S. Leue. 2008. Debugging of Dependability Models Using Interactive Visualization of Counterexamples. Technical Report soft-08-04, Chair for Software Engineering, University of Konstanz. [PDF]
  • W. Wei. 2008. Incomplete Property Checking for Asynchronous Reactive Systems. Doctoral Dissertation, University of Konstanz. [PDF]
  • S. Leue, A. Stefanescu, and W. Wei. 2008. Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes. Proceedings of 15th International SPIN Workshop on Model Checking of Software (SPIN '08), Lecture Notes in Computer Science, Volume 5156. Springer Verlag. [SPIN 2008] [PDF]
  • S. Leue and P. Merino (Eds.). 2008. Formal Methods for Industrial Critical Systems. 12th International Workshop, FMICS 2007, Revised Selected Papers, LNCS 4916, Lecture Notes in Computer Science, Springer Verlag. [FMICS 2007]
  • S. Leue, A. Stefanescu, and W. Wei. 2008. An AsmL Semantics for Dynamic Structures and Run Time Schedulability in UML-RT. Proceedings of 46th International Conference on Objects, Models, Components, Patterns, Lecture Notes in Business and Information Processing, Volume 11. Springer Verlag. [TOOLS 2008] [PDF]
  • H. Aljazzar and S. Leue. 2008. K*: A Directed On-The-Fly Algorithm for Finding the k Shortest Paths. Technical Report soft-08-03, Chair for Software Engineering, University of Konstanz. [PDF]
  • S. Leue, A. Stefanescu, and W. Wei. 2008. An AsmL Semantics for Dynamic Structures and Run Time Schedulability in UML-RT. Technical Report soft-08-02, Chair for Software Engineering, University of Konstanz. [PDF]

2007

  • H. Aljazzar and S. Leue. 2007. Counterexamples for Model Checking of Markov Decision Processes. Technical Report soft-08-01, Chair for Software Engineering, University of Konstanz. [PDF]
  • D. Bosnacki, S. Leue, and A. Lluch Lafuente. 2007. Partial-Order Reduction for General State Exploring Algorithms. International Journal on Software Tools for Technology Transfer (to appear). [Journal] [PDF]

2006

  • G. di Fatta, S. Leue, and E. Stegantova. 2006. Discriminative Pattern Mining in Software Fault Detection. In Proceedings of the Third International Workshop on Software Quality Assurance. ACM Digital Library. [SOQUA 2006] [PDF]
  • H. Aljazzar and S. Leue. 2006. Extended Directed Search for Probabilistic Timed Reachability. In Proceedings of 4th International Conference on Formal Modelling and Analysis of Timed Systems FORMATS '06, LNCS 4137 (pp. 33-51). Springer Verlag. [FORMATS 2006] [PDF]
  • S. Leue, A. Stefanescu, and W. Wei. 2006. A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems. In Proceedings of 17th International Conference on Concurrency Theory CONCUR '06, LNCS 4137 (pp. 79-94). Springer Verlag. [CONCUR 2006] [PDF]
  • H. Aljazzar and S. Leue. 2006. Extended Directed Search for Probabilistic Timed Reachability. Technical Report soft-06-03, Chair for Software Engineering, University of Konstanz. [PDF]
  • S. Leue, A. Stefanescu, and W. Wei. 2006. A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems. Technical Report soft-06-02, Chair for Software Engineering, University of Konstanz. [PDF]
  • D. Bosnacki, S. Leue, and A. Lluch Lafuente. 2006. Partial-Order Reduction for General State Exploring Algorithms. In Proceedings of the 13th International SPIN Workshop on Model Checking of Software, LNCS 3925 (pp. 271-287). Springer Verlag. [SPIN 2006] [PDF]
  • S. Leue and W. Wei. 2006. A Region Graph Based Approach to Termination Proofs. Technical Report soft-06-01, Chair for Software Engineering, University of Konstanz. [PDF]
  • S. Leue and W. Wei. 2006. A Region Graph Based Approach to Termination Proofs. In Proceedings of 12th. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 3920 (pp. 318-333). Springer Verlag. [TACAS 2006] [PDF]

2005

  • D. Bosnacki, S. Leue, and A. Lluch Lafuente. 2005. Partial-Order Reduction for General State Exploring Algorithms. Technical Report soft-05-02, Chair for Software Engineering, University of Konstanz. [PDF]
  • H. Aljazzar, H. Hermanns, and S. Leue. 2005. Counterexamples for Timed Probabilistic Reachability. In Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems, LNCS 3829 (pp. 177-195). Springer Verlag. [FORMATS 2005] [PDF]
  • S. Leue and T. J. Systä (Eds.). Scenarios: Models, Transformations and Tools. Proceedings of International Workshop Dagstuhl Castle, Germany, September 2003, LNCS 3466. Springer Verlag. [Journal]
  • S. Leue and W. Wei. 2005. Counterexample-based Refinement for a Boundedness Test for CFSM Languages. In Proceedings of 12th International SPIN Workshop on Model Checking of Software, LNCS 3639 (pp. 58-74). Springer Verlag. [SPIN 2005] [PDF]
  • S. Leue and W. Wei. 2005. Counterexample Refinement for a Boundedness Test for CFSM Languages. Technical Report soft-05-01, Chair for Software Engineering, University of Konstanz. [PDF]

2004

  • M. Dwyer and S. Leue. 2004. The Algorithmics of Software Model Checking. International Journal on Software Tools for Technology Transfer 6, 4 (2004), 257-259. Springer Verlag. [PDF]
  • J. Tan, G. S. Avrunin, L. A. Clarke, S. Zilberstein, and S. Leue. 2004. Heuristic-Guided Counterexample Search in FLAVERS. In Proceedings of the 12th ACM Symposium on the Foundations of Software Engineering (pp. 201-210). ACM Press. [SIGSOFT 2004] [PDF]
  • S. Edelkamp, S. Leue, and A. Lluch-Lafuente. 2004. Partial-Order Reduction and Trail Improvement in Directed Model Checking. International Journal on Software Tools for Technology Transfer 6, 4 (2004), 277-301. Springer Verlag. [STTT 2004] [PDF]
  • S. Leue, R. Mayr, and W. Wei. 2004. A Scalable Incomplete Test for Message Buffer Overflow in Promela Models. In Proceedings of the 11th International SPIN Workshop on Model Checking Software, LNCS 2989 (pp. 216-233). Springer Verlag. [SPIN 2004] [PDF]
  • S. Leue, R. Mayr, and W. Wei. 2004. A Scalable Incomplete Test for the Boundedness of UML RT Models. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2988 (pp. 327-341). Springer Verlag. [TACAS 2004] [PDF]
  • S. Edelkamp, S. Leue, and A. Lluch-Lafuente. 2004. Directed Explicit-State Model Checking in the Validation of Communication Protocols. International Journal on Software Tools for Technology Transfer 5, 2-3, 247-267. Springer Verlag. [STTT 2004] [PDF]

2003

  • P. Biechele and S. Leue. 2003. Explicit State Model Checking in the Development Process for Inter-locking Software Systems. In Proceedings of the Workshop on Model-Checking for Dependable Software-Intensive Systems at the IEEE/IFIP International Conference on Dependable Systems and Networks, San Francisco, USA. [PDF]

2002

  • D. Bosnacki and S. Leue (Eds.). 2002. Proceedings of the 9th International SPIN Workshop on Model Checking of Software. LNCS 2318, Springer Verlag.
  • A. Lluch-Lafuente, S. Edelkamp, and S. Leue. 2002. Partial Order Reduction in Directed Model Checking. In Proceedings of the 9th International SPIN Workshop on Software Model Checking (LNCS 2318), 112-127, Springer Verlag. [SPIN 2002] [PDF]

2001

  • S. Edelkamp, A. Lluch Lafuente, and S. Leue. 2001. Protocol Verification with Heuristic Search. In Proceedings of the AAAI-Spring Symposium on Model-based Validation of Intelligence, 75-83, Stanford University. [PDF] [PS]
  • S. Edelkamp, A. Lluch Lafuente, and S. Leue. 2001. Directed Explicit Model Checking with HSF-SPIN. In Proceedings of the 8th International SPIN Workshop on Model Checking Software (LNCS 2057), 57-79, Springer Verlag. [SPIN 2001] [PDF] [PS]
  • S. Edelkamp, A. Luch Lafuente, and S. Leue. 2001. Trail-Directed Model Checking. In Proceedings of the Workshop on Software Model Checking, Electronic Notes in Theoretical Computer Science 55 (3), 343-356, Elsevier. [CAV 2001] [PDF]
  • S. Edelkamp, S. Leue, and A. Lluch-Lafuente. 2001. Partial Order Reduction in Directed Model Checking. Technical Report No. 162, Institute for Computer Science, Albert-Ludwigs-University Freiburg. [PDF] [PS]
  • S. Edelkamp, S. Leue, and A. Lluch-Lafuente. 2001. Directed Explicit-State Model Checking in the Validation of Communication Protocols. Technical Report No. 161, Institute for Computer Science, Albert-Ludwigs-University Freiburg. [PDF] [PS]

2000

  • M. Kamel and S. Leue. 2000. Formalization and Validation of the General Inter-ORB Protocol (GIOP) using Promela and Spin. International Journal on Software Tools for Technology Transfer 2 (4), 394-409, Springer Verlag. [STTT 2000] [PDF]
  • M. Kamel and S. Leue. 2000. VIP: A Visual Editor and Compiler for v-Promela. In Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (LNCS 1785), 471-486, Springer Verlag. [TACAS 2000] [PDF] [PS]

1999

  • P. Tysowski, M. Zulkernine, and S. Leue. 1999. JaCal: An Implementation of Linda in Java. In Proceedings of the IASTED Conference on Parallel and Distributed Computing and Systems PDCS '99, 683-692, Cambridge. [PDF]
  • D. Dams, R. Gerth, S. Leue, and M. Massink (Eds.). 1999. Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking (LNCS 1680), Springer Verlag.
  • S. Leue and G. Holzmann. 1999. v-Promela: A Visual, Object-Oriented Language for Spin. In Proceedings of the Second IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, 14-23, Saint Malo, France, IEEE Computer Society Press. [ISORC 1999] [PDF]

1998

  • M. Kamel and S. Leue. 1998. Validation of Remote Object Invocation and Object Migration in CORBA GIOP using Promela/Spin. In Actes/Proceedings Spin\'98, Ecole Nationale Superieure des Telecommunications, Paris, France. [PDF]
  • H. Ben-Abdallah and S. Leue. 1998. MESA: Support for Scenario-Based Design of Concurrent Systems. In Lecture Notes in Computer Science (Volume 1384), 118-135, Springer Verlag.
  • [PDF] [PS]
  • H. Ben-Abdallah and S. Leue. 1998. MESA: Support for Scenario-Based Design of Concurrent Systems. In Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. [TACAS 1998] [PDF] [PS]
  • S. Leue, L. Mehrmann, and M. Rezai. 1998. Synthesizing ROOM Models from Message Sequence Chart Specifications. In 13th IEEE Conference on Automated Software Engineering, Honolulu, Hawaii. [PDF] [PS]
  • S. Leue, L. Mehrmann, and M. Rezai. 1998. Synthesizing ROOM Models from Message Sequence Chart Specifications. Technical Report 98-06, Dept. of Electrical and Computer Engineering, University of Waterloo. [PDF] [PS]

1997

  • S. Fischer and S. Leue. 1997. Formal Methods for Broadband and Multimedia Systems. Technical Report 97-08, Department of Electrical and Computer Engineering, University of Waterloo. [PDF] [PS]
  • S. Fischer and S. Leue. 1997. Formal Methods for Broadband and Multimedia Systems. In Computer Networks and ISDN Systems. [PDF] [PS]
  • P.B. Ladkin and S. Leue. 1997. Implementing and Verifying MSC Specifications Using Promela/XSpin. In Proceedings of the DIMACS Workshop SPIN96, the 2nd International Workshop on the SPIN Verification System (Volume 32), DIMACS Series, American Mathematical Society, Providence, R.I. [PDF] [PS]
  • Ladkin, P. B. and Leue, S. 1997. Implementing and Verifying MSC Specifications Using Promela/XSpin. DIMACS Series, 32, Proceedings of the DIMACS Workshop SPIN96, the 2nd International Workshop on the SPIN Verification System. American Mathematical Society, Providence, R.I. [PDF]
  • Ben-Abdallah, H. and Leue, S. 1997. Timing Constraints in Message Sequence Chart Specifications. Formal Description Techniques X, Proceedings of the Tenth International Conference on Formal Description Techniques FORTE/PSTV'97. Chapman & Hall. [FORTE 1997] [PDF]
  • Ben-Abdallah, H. and Leue, S. 1997. Syntactic Detection of Process Divergence and non-Local Choice in Message Sequence Charts. Lecture Notes in Computer Science, 1217, 259-274. Springer Verlag. [PDF] [PS]
  • Ben-Abdallah, H. and Leue, S. 1997. Syntactic Detection of Process Divergence and non-Local Choice in Message Sequence Charts. Proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. [TACAS 1997] [PDF]
  • Ben-Abdallah, H. and Leue, S. 1997. Expressing and Analyzing Timing Constraints in Message Sequence Chart Specifications. Technical Report 97-04. Dept. of Electrical and Computer Engineering, University of Waterloo. [PDF]

1996

  • Ladkin, P. B. and Leue, S. 1996. Implementing and Verifying Scenario-Based Specifications Using Promela/XSpin. Participants Proceedings of the Second SPIN Workshop. Rutgers University, New Brunswick, New Jersey. [PDF] [PS]
  • Ben-Abdallah, H. and Leue, S. 1996. Architecture of a Requirements and Design Tool Based on Message Sequence Charts. Technical Report 96-13. Dept. of Electrical and Computer Engineering, University of Waterloo. [PDF] [PS]
  • Ben-Abdallah, H. and Leue, S. 1996. Syntactic Analysis of Message Sequence Chart Specifications. Technical Report 96-12. Dept. of Electrical and Computer Engineering, University of Waterloo. [PDF] [PS]
  • Leue, S. and Oechslin, Ph. Opparim - A Method and Tool for Optimized Parallel Protocol Implementation. Journal of High Speed Networks, 5, 125-143, 1996. [HSN 1996] [PDF] [PS]
  • Leue, S. and Oechslin, Ph. On Parallelising and Optimising the Implementation of Communication Protocols. IEEE/ACM Transactions on Networking, 4(1), 55-70, 1996. [IEEE 1996] [PDF] [PS]

1995

  • Ladkin, P. B. and Leue, S. 1995. Four Issues Concerning the Semantics of Message Flow Graphs. Formal Description Techniques VII, Proceedings of the Seventh IFIP International Conference on Formal Description Techniques FORTE'94. Chapman & Hall. [FORTE 1994] [PDF]
  • Ladkin, P. B. and Leue, S. 1995. Comments on a Proposed Semantics for Basic Message Sequence Charts. The Computer Journal, 37(9). [PDF]
  • Ladkin, P. B. and Leue, S. 1995. Implementing Message Sequence Charts in Promela. Proceedings of the First SPIN Workshop. Montreal, Canada. [PDF]
  • Ladkin, P. B. and Leue, S. 1995. Interpreting Message Flow Graphs. Formal Aspects of Computing, 7(5), 473-509. [PDF]
  • Leue, S. Specifying Real-Time Requirements for SDL Specifications - A Temporal Logic-Based Approach. Proceedings of the Fifteenth International Symposium on Protocol Specification, Testing, and Verification PSTV'95, Chapman & Hall, 1995. [PSTV 1995] [PDF] [PS]
  • Hogrefe, D. and Leue, S (Ed.): Formal Description Techniques VII - Proceedings of the Seventh IFIP International Conference on Formal Description Techniques FORTE'94, Proceedings of the Seventh IFIP International Conference on Formal Description Techniques FORTE'94, Chapman & Hall, 1995.

1994

  • Leue, S. Methods and Semantics for Telecommunications Systems Engineering. Doctoral Dissertation, University of Berne, 1994. [PDF] [PS]
  • Ladkin, P. B. and Leue, S. 1994. What Do Message Sequence Charts Mean? Formal Description Techniques VI, IFIP Transactions C, Proceedings of the 6th International Conference on Formal Description Techniques. [PDF] [PS]
  • Leue, S. and Oechslin, Ph. Enhancing Integrated Layer Processing using Common Case Anticipation and Data Dependence Analysis. Proceedings of the First International Workshop on High Performance Protocol Architectures HIPPARCH '94, INRIA Sophia Antipolis, 1994. [PDF] [PS]
  • Leue, S. and Oechslin, Ph. Formalizations and Algorithms for Optimized Parallel Protocol Implementation. Proceedings of the IEEE International Conference on Network Protocols ICNP-94, IEEE Computer Society Press, Boston, Massachusetts, 1994. [ICNP 1994] [PDF] [PS]
  • Leue, S. and Oechslin, Ph. From SDL Specification to Optimized Parallel Protocol Implementations. Proceedings of the Fourth International IFIP Workshop on Protocols for High-Speed Networks, Chapman & Hall, 1994. [PfHSN 1994] [PDF] [PS]
  • Leue, S. QoS Specification Based on SDL/MSC and Temporal Logic. Proceedings of the Montreal Workshop on Multimedia Applications and Quality of Service Verification, Montreal, 1994. [PDF] [PS]

1993

  • Leue, S. and Oechslin, Ph. Optimization Techniques for Parallel Protocol Implementation. Proceedings of the Fourth Workshop on Future Trends of Distributed Computing Systems, IEEE Computer Society Press, 1993. [DCS 1993] [PDF] [PS]
  • Ladkin, P. B. and Leue, S. 1993. Interpreting Message Sequence Charts (revised version). Technical Report TR 101. Dept. of Computing Science, University of Stirling, United Kingdom
  • Ladkin, P. B. and Leue, S. 1993. On the Semantics of Message Sequence Charts. Formale Methoden für Verteilte Systeme. K.G. Sauer-Verlag, München. ISBN: 3-598-22409-5. [PDF]

1992

  • Ladkin, P. B. and Leue, S. 1992. Interpreting Message Sequence Charts. Research Report RJ 8965. IBM Almaden Research Center.