Publications of Viktor Schuppan

(Preprints are provided for personal use only. Please respect the respective publisher's copyright and use publisher's version where possible.)

Temporal Logic Synthesis

[BCG+10] R. Bloem, A. Cimatti, K. Greimel, G. Hofferek, R. Könighofer, M. Roveri, V. Schuppan, R. Seeber: RATSY - A New Requirements Analysis Tool with Synthesis. In: T. Touili, B. Cook, P. Jackson (eds.): Proceedings of the 22nd International Conference on Computer Aided Verification (CAV 2010), Edinburgh, UK, July 15-19, 2010. Volume 6174 of Lecture Notes in Computer Science, pp. 425-429. Springer, 2010. doi:10.1007/978-3-642-14295-6_37. Acceptance rate: 17 out of 44 tool submissions (38 %). Download: publisher, preprint (zipped), BibTeX
[CRST08] A. Cimatti, M. Roveri, V. Schuppan, A. Tchaltsev: Diagnostic Information for Realizability. In: F. Logozzo, D. Peled, L. Zuck (eds.): Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2008), San Francisco, CA, USA, January 7-9, 2008. Volume 4905 of Lecture Notes in Computer Science, pp. 52-67. Springer, 2008. doi:10.1007/978-3-540-78163-9_9. Acceptance rate: 21 out of over 60 (< 35 %). Download: publisher, preprint (zipped), BibTeX, experiments

Temporal Logic Satisfiability

[Sch16] V. Schuppan: Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance. In: N. Bertrand, L. Bortolussi and H. Wiklicky (eds.): Quantitative Aspects of Programming Languages and Systems (2013-14), Theoretical Computer Science 655, Part B: pp. 155-192. Elsevier, 2016. doi:10.1016/j.tcs.2016.01.014. Substantially extended version of [Sch13b]. Download: publisher, preprint (zipped), full (zipped), BibTeX, tool, web page with experimental results
[Sch15] V. Schuppan: Extracting Unsatisfiable Cores for LTL via Temporal Resolution. In: C. Sanchez, B. Venable, E. Zimanyi (eds.): Special Issue: Temporal Representation and Reasoning (TIME'13) - Part 2, Acta Informatica 53 (3) 2016: pp. 247-299. Springer, 2015. doi:10.1007/s00236-015-0242-1. Invited, substantially extended version of [Sch13c]. Download: publisher, preprint (zipped), full (zipped), BibTeX, tool, web page with experimental results
[Sch13c] V. Schuppan: Extracting Unsatisfiable Cores for LTL via Temporal Resolution. In: C. Sanchez, B. Venable, E. Zimanyi (eds.): Proceedings of the 20th International Symposium on Temporal Representation and Reasoning (TIME 2013), Pensacola, FL, USA, September 26-28, 2013, pp. 54-61. IEEE Computer Society, 2013. doi:10.1109/TIME.2013.15. Acceptance rate: 15 out of 26 submissions (58 %). For the journal version see [Sch15], for an earlier version see [Sch12b]. Download: publisher, preprint (zipped), full (zipped), BibTeX, slides, tool, web page with experimental results
[Sch13b] V. Schuppan: Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance. In: L. Bortolussi, H. Wiklicky (eds.): Proceedings of the Eleventh International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013), Rome, Italy, March 23-24, 2013. Volume 117 of Electronic Proceedings in Theoretical Computer Science, pp. 49-65. Open Publishing Association, 2013. For the preliminary proceedings version see [Sch13a]. Download: publisher, local (zipped), full (zipped), BibTeX, tool, web page with experimental results
[Sch13a] V. Schuppan: Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance. In: L. Bortolussi, H. Wiklicky (eds.): Preliminary Proceedings of the Eleventh International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013), Rome, Italy, March 23-24, 2013. For the (post-) proceedings version see [Sch13b]. Download: preprint (zipped), BibTeX, slides, tool, web page with experimental results
[Sch12b] V. Schuppan: Extracting Unsatisfiable Cores for LTL via Temporal Resolution. For a peer reviewed, updated version see [Sch13c]. Download: arXiv:1212.3884v1 [cs.LO], local (zipped), BibTeX, tool, web page with experimental results
[Sch12a] V. Schuppan: Towards a Notion of Unsatisfiable and Unrealizable Cores for LTL. In: G. Salaün, F. Arbab, M. Sirjani (eds.): Selected Papers from Foundations of Coordination Languages and Software Architectures (FOCLASA'09), Selected Papers from Fundamentals of Software Engineering (FSEN'09), Science of Computer Programming 77 (7-8) 2012: pp. 908-939. Elsevier, 2012. doi:10.1016/j.scico.2010.11.004. Invited, substantially extended version of [Sch10], [Sch09a]. Download: publisher, preprint (zipped), BibTeX
[SD11] V. Schuppan, L. Darmawan: Evaluating LTL Satisfiability Solvers. In: T. Bultan, P.-A. Hsiung (eds.): Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA 2011), Taipei, Taiwan, October 11-14, 2011. Proceedings. Volume 6996 of Lecture Notes in Computer Science, pp. 397-413. Springer, 2011. doi:10.1007/978-3-642-24372-1_28. Acceptance rate: 23 regular papers (+ 11 short papers and 2 tool papers) out of 75 submissions (31 %). Download: publisher, preprint (zipped), full version (zipped), BibTeX, slides, web page with data, benchmarks, etc
[Sch10] V. Schuppan: Towards a Notion of Unsatisfiable Cores for LTL. In: F. Arbab, M. Sirjani (eds.): Fundamentals of Software Engineering, Third IPM International Conference, FSEN 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected Papers. Volume 5961 of Lecture Notes in Computer Science, pp. 129-145. Springer, 2010. doi:10.1007/978-3-642-11623-0_7. For the journal version see [Sch12a], for the pre-proceedings version see [Sch09a]. Download: publisher, local (zipped), BibTeX
[Sch09a] V. Schuppan: Towards a Notion of Unsatisfiable Cores for LTL. In: F. Arbab, M. Sirjani (eds.): Pre-Proceedings of the 3rd International Conference on Fundamentals of Software Engineering (FSEN 2009), Kish Island, Persian Gulf, Iran, April 15-17, 2009, pp. 57-72. Acceptance rate: 22 regular papers (+ 5 short papers and 7 poster presentations) out of 88 submissions (25 %). Best Paper Award. For the journal version see [Sch12a], for the post-proceedings version see [Sch10]. Download: preprint (zipped), BibTeX, slides
[Sch09b] V. Schuppan: Towards a Notion of Unsatisfiable Cores for LTL. Technical Report 200901000, Fondazione Bruno Kessler, 2009. Technical report version of [Sch09a], [Sch10]. Download: preprint (zipped), BibTeX
[CRST07] A. Cimatti, M. Roveri, V. Schuppan, S. Tonetta: Boolean Abstraction for Temporal Logic Satisfiability. In: W. Damm, H. Hermanns (eds.): Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), Berlin, Germany, July 3-7, 2007. Volume 4590 of Lecture Notes in Computer Science, pp. 532-546. Springer, 2007. doi:10.1007/978-3-540-73368-3_53. Acceptance rate: 33 out of 134 (25 %). Download: publisher, preprint (zipped), extended version (zipped), BibTeX, slides, experiments and full set of plots

Model Checking

[ESB+09] S. Edelkamp, V. Schuppan, D. Bosnacki, A. Wijs, A. Fehnker, H. Aljazzar: Survey on Directed Model Checking. Invited contribution (not peer-reviewed). In: D. Peled, M. Wooldridge (eds.): 5th International Workshop on Model Checking and Artificial Intelligence (MoChArt 2008), Revised Selected and Invited Papers, Patras, Greece, July 21, 2008. Volume 5348 of Lecture Notes in Computer Science, pp. 65-89. Springer, 2009. doi:10.1007/978-3-642-00431-5_5. Download: publisher, preprint (zipped), BibTeX
[BHJ+06] A. Biere, K. Heljanko, T. Junttila, T. Latvala, V. Schuppan: Linear Encodings of Bounded LTL Model Checking. In: K. Etessami, S. Rajamani (eds.): Selected Papers of the Conference "Computer Aided Verification 2005", Logical Methods in Computer Science 2 (5:5) 2006. doi:10.2168/LMCS-2(5:5)2006. Download: publisher, preprint (zipped), BibTeX
[SB05a] V. Schuppan, A. Biere: Shortest Counterexamples for Symbolic Model Checking of LTL with Past. In: N. Halbwachs, L. Zuck (eds.): Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Edinburgh, UK, April 4-8, 2005. Volume 3440 of Lecture Notes in Computer Science, pp. 493-509. Springer, 2005. doi:10.1007/978-3-540-31980-1_32. Acceptance rate: 33 out of 141 (23 %). For the full version see [SB05c]. Download: publisher, preprint (zipped), BibTeX, slides, SMV models
[SB05b] V. Schuppan, A. Biere: Liveness Checking as Safety Checking for Infinite State Spaces. In: S. Smolka and J. Srba (eds.): Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY 2005), San Francisco, CA, USA, August 27, 2005. Electronic Notes in Theoretical Computer Science 149 (1), pp. 79-96. Elsevier, 2006. doi:10.1016/j.entcs.2005.11.018. Full version of [SB05d]. Download: publisher, preprint (zipped), BibTeX
[SB05c] V. Schuppan, A. Biere: Shortest Counterexamples for Symbolic Model Checking of LTL with Past. Technical Reports 470, ETH Zürich, Department of Computer Science, 01/2005. Full version of [SB05a]. Download: publisher, preprint (zipped), BibTeX
[SB05d] V. Schuppan, A. Biere: Liveness Checking as Safety Checking for Infinite State Spaces. In: S. Smolka and J. Srba (eds.): Preliminary Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY 2005), San Francisco, CA, USA, August 27, 2005, pp. 53-64. For the full version see [SB05b]. Download: publisher, preprint (zipped), BibTeX, slides
[SB04] V. Schuppan, A. Biere: Efficient reduction of finite state model checking to reachability analysis. In: International Journal on Software Tools for Technology Transfer (STTT) (2004) 5: pp. 185-204. Springer, 2004. doi:10.1007/s10009-003-0121-x. Substantially extended and corrected version of [BAS02]. Download: publisher, preprint (zipped), BibTeX, SMV models
[BAS02] A. Biere, C. Artho, V. Schuppan: Liveness Checking as Safety Checking. In: R. Cleaveland, H. Garavel (eds.): Proceedings of the Seventh International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2002), Malaga, Spain, July 12-13, 2002. doi:10.1016/S1571-0661(04)80410-9. Acceptance rate: 13 out of 22 (59 %). For a substantially extended and corrected version see [SB04]. Download: publisher, preprint (zipped), BibTeX, slides

Java Checking

[ABH+06] C. Artho, A. Biere, S. Honiden, V. Schuppan, P. Eugster, M. Baur, B. Zweimüller, P. Farkas: Advanced Unit Testing - How to Scale Up a Unit Test Framework. In: Proceedings of the 1st International Workshop on Automation of Software Test (AST 2006), Shanghai, China, May 23, 2006, pp. 92-98. ACM Press, 2006. doi:10.1145/1138929.1138947. Download: publisher, preprint (zipped), BibTeX
[ASB+04] C. Artho, V. Schuppan, A. Biere, P. Eugster, M. Baur, B. Zweimüller: JNuke: Efficient Dynamic Analysis for Java. In: R. Alur, D. Peled (eds.): Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), Boston, MA, USA, July 13-17, 2004. Volume 3114 of Lecture Notes in Computer Science, pp. 462-465. Springer, 2004. doi:10.1007/978-3-540-27813-9_37. Download: publisher, preprint (zipped), BibTeX
[SBB04] V. Schuppan, M. Baur, A. Biere: JVM Independent Replay in Java. In: K. Havelund, G. Rosu (eds.): Proceedings of the Fourth Workshop on Runtime Verification (RV 2004), Barcelona, Spain, April 3-4, 2004. Volume 113 of Electronic Notes in Theoretical Computer Science, pp. 85-104. Elsevier, 2005. doi:10.1016/j.entcs.2004.01.032. Acceptance rate: 11 out of 13 (85 %). Download: publisher, preprint (zipped), BibTeX, slides

Case Study: IEEE 1394 FireWire

[SB03] V. Schuppan, A. Biere: Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV. In: Formal Aspects of Computing (2003) 14: pp. 267-280. Springer, 2003. doi:10.1007/s001650300005. Extended version of [SB01]. Download: publisher, preprint (zipped), BibTeX, SMV models
[SB01] V. Schuppan, A. Biere: A Simple Verification of the Tree Identify Protocol with SMV. In: S. Maharaj, J. Romijn, C. Shankland (eds.): Proceedings of the IEEE 1394 (FireWire) Workshop, pp. 31-34, Berlin, Germany, March 13, 2001. Department of Computing Science and Mathematics, University of Stirling, March 2001. For an extended version see [SB03]. Download: full text (zipped), BibTeX, slides

Evaluating V-Model 97 with CMM

[SR00] V. Schuppan, W. Rußwurm: A CMM-Based Evaluation of the V-Model 97. In: R. Conradi (ed.), Proceedings of the 7th European Workshop on Software Process Technology (EWSPT 2000), Kaprun, Austria, February 21-25, 2000. Volume 1780 of Lecture Notes in Computer Science, pp. 69-83. Springer, 2000. doi:10.1007/BFb0095015. Acceptance rate: 21 out of 44 (48 %). Download: publisher, preprint (zipped), BibTeX
[SR99] V. Schuppan, W. Rußwurm: Das V-Modell 97 auf dem Weg zum CMM-konformen Standard (The V-Model 97 aiming to become CMM-compliant standard). In: Software@Siemens, December 1999: pp. 40-42. Siemens AG, 1999. Download: scan (zipped), BibTeX. A shorter version also appeared in the English edition: Software@Siemens, February 2000: pp. 54-55. Siemens AG, 2000. Download: scan (zipped), BibTeX

Theses

[Sch06] V. Schuppan: Liveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties (Ph.D. thesis). Diss. ETH No. 16268, Swiss Federal Institute of Technology, 2006. Published by Verlag Dr. Hut, Munich, Germany, ISBN 3-89963-337-7, 2006. Download: ETH E-Collection, PDF (zipped), BibTeX, slides (defense)
[Sch99] V. Schuppan: Das V-Modell 97 als Softwareentwicklungsprozeß aus der Sicht des Capability Maturity Models (CMM) für Software (Master's thesis). Diplomarbeit, Institut für Informatik, Technische Universität München, 1999. Download: full text (zipped), BibTeX

Other

[Sch97] V. Schuppan: Verschlüsselungsfreiheit soll eingeschränkt werden (Encryption to be controlled). In: impulsiv, Nr. 57, May 1997: p. 7. Fachschaft Math/Phys/Info. (Student magazine for maths/physics/CS students at TU München). Download: publisher, scan (zipped). A shorter version also appeared in: PANIK, Ausgabe 23, June 1997: p. 21. Studentische Vertretung der TU München. (Student magazine for all students at TU München). Download: scan (zipped)