talks

[1]: Joshua Rowe, Markus A. Kuppe, and Finn Hackett. Understanding Inconsistency in Azure CosmosDB with TLA+. page Submitted, 2023. [ bib ]
[2]: Markus A. Kuppe. Teaching TLA+ in Industry. Tutorial Series of the FME Teaching Committee, December 2022. [ bib | http ]
[3]: Stephan Merz, Igor Konnov, and Markus A. Kuppe. Specification and Verification wth the TLA+ Trifecta: TLC, Apalache, and TLAPS. SpecifyThis at ISoLA, page To Appear, November 2022. [ bib ]
[4]: Jack Valightly and Markus A. Kuppe. Obtaining statistical propertiesby simulating specs with TLC. TLA+ Conference, September 2022. [ bib | http ]
[5]: Markus A. Kuppe. The TLA+ Debugger. F-IDE 2022, page To Appear, September 2022. [ bib | http ]
[6]: Markus A. Kuppe. Workshop: TLA+ in Action - blocking Queue. Distributed Systems Meetup Bangaluru, August 2022. [ bib | http ]
[7]: Markus A. Kuppe. Workshop: TLA+ in Action - blocking Queue. MCH2022, July 2022. [ bib | http ]
[8]: Joshua Rowe, Markus A. Kuppe, and Finn Hackett. Understanding inconsistency in azure cosmos db with tla+. Microsoft Internal (Cloud Reliability RIA all-hands), July 2022. [ bib ]
[9]: Markus A. Kuppe. Tla+: The tools, the language, the application. Invited Talk at University of British Columbia (UBC), Canada, June 2022. [ bib ]
[10]: Markus A. Kuppe. Tla+ in 5 minutes. Microsoft Internal (RiSE all-hands), June 2022. [ bib ]
[11]: Markus A. Kuppe. Let's shift-shift left: How modeling can help software engineering. Microsoft Internal (Storytelling Workshop), May 2022. [ bib | http ]
[12]: Markus A. Kuppe. Cloud reliability::tla+. Microsoft Internal (RiSE all-hands), May 2022. [ bib ]
[13]: Markus A. Kuppe. Weeks of debugging can save you hours of tla+. Microsoft Internal (Cloud Talks), May 2022. [ bib ]
[14]: Markus A. Kuppe. Tlc changelog. Microsoft Internal (Brown Bag), April 2022. [ bib ]
[15]: Markus A. Kuppe. Weeks of debugging can save you hours of tla+. Microsoft Internal (CODE Conf), March 2022. [ bib ]
[16]: Markus A. Kuppe. Weeks of debugging can save you hours of tla+ (extended version). Distributed Systems Meetup Pune, February 2022. [ bib | http ]
[17]: Markus A. Kuppe. Rise4fun & profit - github codespaces & vscode. Microsoft Internal (RiSE all-hands), February 2022. [ bib ]
[18]: Markus A. Kuppe. Shift-shift-left design. Microsoft Internal (Cloud Reliability RIA all-hands), February 2022. [ bib ]
[19]: Markus A. Kuppe. Rise4fun. Microsoft Internal (RiSE all-hands), January 2022. [ bib ]
[20]: Markus A. Kuppe. Weeks of debugging can save you hours of tla+. Detroit Tech Watch Meetup, January 2022. [ bib | http ]
[21]: Markus A. Kuppe. Workshop: Tla+ in action. Strange Loop Workshop, September 2021. [ bib ]
[22]: Markus A. Kuppe. Workshop: Tla+ in action. Strange Loop Workshop, September 2021. [ bib ]
[23]: Leslie Lamport and Markus A. Kuppe. Tla+ : Viewed from 40,000 feet and ground level. LinkedIn Internal (Tech Talk Series), August 2021. [ bib ]
[24]: Markus A. Kuppe. Workshop: Tla+ in action, June 2021. [ bib | http ]
[25]: Markus A. Kuppe. Weeks of debugging can save you hours of tla+. In SREcon20 Americas (SREcon20 Americas). USENIX Association, December 2020. [ bib | http ]
[26]: Markus A. Kuppe. Tla+. Microsoft Internal (RiSE all-hands), December 2020. [ bib ]
[27]: Markus A. Kuppe. Tla+ meets azure bootcamp. Microsoft Internal (BrownBag), November 2020. [ bib ]
[28]: Leslie Lamport and Markus A. Kuppe. Tla+ : Viewed from 40,000 feet and ground level. Microsoft Internal (Speaker Series), October 2020. [ bib ]
[29]: Markus A. Kuppe. Tla+ meets azure bootcamp. Microsoft Internal (BrownBag), September 2020. [ bib ]
[30]: Markus A. Kuppe. Tla+ meets azure bootcamp. Microsoft Internal (BrownBag), August 2020. [ bib ]
[31]: Markus A. Kuppe. Tla+ meets azure bootcamp. Microsoft Internal (BrownBag), July 2020. [ bib ]
[32]: Markus A. Kuppe. Tla+ meets azure bootcamp. Microsoft Internal (Bootcamp), July 2020. [ bib | http ]
[33]: Markus A. Kuppe. Tla+ meets mrs healthcare. Microsoft Internal (BrownBag), June 2020. [ bib | http ]
[34]: Markus A. Kuppe. Tla+ at techfest. Microsoft Internal (TechFest), April 2020. Accepted - Cancelled due to Covid19. [ bib | http ]
[35]: Markus A. Kuppe. Weeks of debugging can save you hours of tla+. CodeStock, April 2020. Talk accepted - Conference cancelled due to Covid19. [ bib ]
[36]: Markus A. Kuppe. Weeks of debugging can save you hours of tla+. Usenix SRE Con West, March 2020. Talk accepted - Conference cancelled due to Covid19. [ bib ]
[37]: Markus A. Kuppe. Tla+: The tools, the language, the application. Invited Talk at Penn State University, Host: Prof George Kesidis, February 2020. [ bib ]
[38]: Markus A. Kuppe. Tla+: The tools, the language, the application. Invited Talk at University of Buffalo, Host: Prof Murat Demirbas, February 2020. [ bib ]
[39]: Markus A. Kuppe. Tla+ meets microsoft avere. Microsoft Internal (BrownBag), February 2020. [ bib | http ]
[40]: Markus A. Kuppe. Msr central engineering pitch tank. Microsoft Internal, January 2020. [ bib ]
[41]: Markus A. Kuppe. Tla+ meets java@microsoft. Microsoft Internal (BrownBag), December 2019. [ bib | http ]
[42]: Markus Alexander Kuppe, Leslie Lamport, and Daniel Ricketts. The tla+ toolbox. Electronic Proceedings in Theoretical Computer Science, 310:50–62, December 2019. [ bib | DOI | http ]
[43]: Markus A. Kuppe. Tla+ meets azure bootcamp. Microsoft Internal (BootCamp), November 2019. [ bib ]
[44]: Markus A. Kuppe. The tla+ toolbox. F-IDE 2019, October 2019. [ bib | http ]
[45]: Markus A. Kuppe. #70 intro to tla+ & formal smart contract design specification. Let's Talk ETC! Podcast, March 2019. [ bib | http ]
[46]: Markus A. Kuppe. Debuggable design with tla+. Hyperscale Verification, March 2019. [ bib | .pdf ]
[47]: Markus A. Kuppe. Let tla+ rise. RiSE group all-hands meeting, August 2018. [ bib | .pdf ]
[48]: Markus A. Kuppe. State space explosion or: How to fight an uphill battle (tutorial). TLA+ Community Event (co-located with FM 2018), July 2018. http://tla2018.loria.fr/. [ bib | http ]
[49]: Markus A. Kuppe. Mit tla+ zum korrekten parallelprogramm. parallel 2018, July 2018. [ bib | .pdf ]
Parallele Programmierung ist ein zentraler Baustein, um immer leistungsfähigere Software zu entwickeln. Parallele Programmierung ist aber auch komplex und fehleranfällig. Das Finden von Concurrency Bugs gleicht einer Suche nach der Nadel im sprichwörtlichen Heuhaufen; ein Heuhaufen der mit jeder Ausführung des Programms durchgewirbelt wird.
Nachdem auf der Parallel18 mit Hilfe von TLA+ bereits ein sporadisch auftretendes Deadlock in einem BoundedBuffer analysiert und behoben wurde, werden in diesem Jahr – nach einer kurzen Einführung in die Grundlagen von TLA+ – die weiterführenden Konzepte von TLA+ vorgestellt. Insbesondere werden neben den Korrektheitsanforderungen, auch Lebendigkeitsanforderungen an den BoundedBuffer formuliert.
Dies erfordert die Einführung von Fairness-Garantien. Kurzum, im Rahmen eines exemplarischen Entwicklungsablaufs wird der typische Einsatz von TLA+ anhand eines einfachen Programms gezeigt. Es werden sowohl der Einstieg als auch die weiterführenden Möglichkeiten von TLA+ vermittelt.
[50]: Markus A. Kuppe. Weeks of debugging can save you hours of tla+. Java User Group hamburg, June 2018. [ bib | http ]
[51]: Markus A. Kuppe. Large scale model checking 101. TLA+ Workshop: Presentations, April 2018. [ bib | http ]
[52]: Markus A. Kuppe. A verified and scalable hash table for the tlc model checker towards an order of magnitude speedup. Master's thesis, University of Hamburg, 2017. Grade 1.0. [ bib | .pdf ]
The applicability of explicit state model checking is restricted by the state space explosion problem which makes the verification of large scale models infeasible. An approach to mitigate state space explosion, is to scale up and benefit from today's multi-core computers. According to Gunther's universal scalability law, scalability is constrained by contention and coherence. For breadth-first model checking with TLC, contention is already minimal. Consequently, we analyze the effects of coherence on TLC's scalability and present a lock-free hash-table algorithm for a model checker's set of seen states. Contrary to most hash-table algorithms present in model checkers, ours is not memory bound. It can be extended to disk. We verify the correctness of our algorithm with TLC. We provide a production-ready implementation of the algorithm in Java for which we demonstrate and quantify superior performance and scalability over TLC's legacy set of seen states. We then propose two additional algorithms for the set of unseen states and the state forest, for which we also include prototypic implementations. When we combine all our proposed changes into TLC, its scalability then exceeds that of SPIN. Our work on TLC's scalability also reveals that the popular approach of lock-striping does not scale. This result is of interest as an argument in favor of lock-free programming, despite its inherent complexity.
[53]: Markus A. Kuppe. Distributed tlc. TLA+ Community Event (co-located with ABZ 2014), June 2014. http://tla2014.loria.fr/. [ bib | .pdf ]
[54]: Markus A. Kuppe. Discover remote services. Eclipse Democamp Hamburg, November 2013. [ bib | http | .pdf ]
[55]: Lars Vogel and Markus A. Kuppe. Become an eclipse committer in 20 min and fork the eclipse ide. Presentation at EclipseCon Europe 2013, Ludwigsburg, Germany, October 2013. [ bib | http | .pdf ]
The Eclipse SDK is available via Git and the common build infrastructure allows to build your own Eclipse IDE. Join this talk to learn how you can checkout the Eclipse IDE source code, modify it, commit your changes and build the Eclipse SDK using CBI and Maven / Tycho. If you follow the approach described in this talk can learn how to build your own Eclipse IDE flavor to test your own developments before contributing them back to Eclipse.
[56]: Markus A. Kuppe and Wim Jongman. Discover remote osgi services. Presentation at EclipseCon Europe 2013, Ludwigsburg, Germany, October 2013. [ bib | http | .pdf ]
The current state of Service Oriented Architecture (SOA) is intimidating. The set of standards invented to "make your life easier" has been growing like wildfire: xml, soap, wadl, widl, wsdl, rest, bics, wxscm, sscm, web.xml, ramp, etcetera etcetera. On top of these protocols you can use a wealth of tooling and frameworks to such an extend that even you, the tech, don't know what is going on... Sometimes you wish that remote services were simple. Just implement an API, expose this API as a service in your OSGi runtime and let network clients use this implementation. If you could only focus on the meat and not on the infrastructure then you could be on your way to solve your business problems instead of solving configurations. This talk explains how the ECF project will take your existing OSGi service and promote it to a network service. The network service will be peer to peer or it will be registered with a discovery server and advertised to any interested clients. The clients then can use the service as if it was a local service. ECF has implemented the new OSGi RSA specification in order to achieve this. ECF committers Markus Kuppe and Wim Jongman will entertrain you on this remote services discovery tour which will include live coding. We will demonstrate how to promote an OSGi service to a remote service. Together we will build a simple remote service and see how all the remote services will be consumed by our client.
[57]: Markus. A. Kuppe. Current state of distributed tlc. International Workshop on the TLA+ Method and Tools, August 2012. [ bib | .pdf | .pdf ]
[58]: Markus A. Kuppe and Wim Jongman. Fun with remote services. Presentation at Eclipse Summit Europe, November 2010. [ bib | http ]
Two complex disciplines in Software Development are Service Architecture and Distributed Programming. Being able to quickly deliver robust applications that use these two techniques is difficult. And this in turn can reduce fun. In this short talk we are going to show you how the Eclipse Communication Framework Project (ECF) and OSGi have managed to simplify both techniques. It shows that even mortal programmers have the ability to quickly create applications that are both SOA and Distributed. This means more focus on the domain and less focus on the technique. We aim to demonstrate how easy it is to use the ECF implementations of the OSGi Remote Services Specification. After this we take it one step further and we will show you how you can add the ECF discovery mechanism. This will eliminate the need for wiring consumers and providers together which reduces overall system administration. During the talk we will also discuss Distributed Programming best practices, pitfalls and nice-to-knows. We will touch stuff like Timing, Async vs Sync calls, Futures and Callbacks. Confused about Eclipse Distributed Programming? You won't be after this episode of "Fun with Remote Services"
[59]: Markus A. Kuppe. Entwicklung verteilter eclipse rcp & osgi anwendungen mit dem eclipse communication framework. Full day tutorial at University of Hamburg Summerschool, October 2010. [ bib | http | .pdf ]
[60]: Markus. A. Kuppe. Soa governance. February 2010. [ bib | .pdf ]
Governance-Modelle spielen auf allen Ebenen eines Unternehmens eine immer staerker werdende Rolle. Sie dienen dabei sowohl der Optimierung der organisatorischen Ablaeufe als auch der optimalen Ausnutzung technischer (IT) Mittel. Die Autoren Weill und Ross (2004) haben gezeigt, dass Unternehmen mit einer funktionierenden (IT) Governance groesseere Gewinne erzielen, als Konkurrenten ohne (IT) Governance. Unter der Annah- me, dass diese Erkenntnis nicht nur fuer IT Governance gilt, sondern sich auch auf die SOA Governance uebertragen laesst, sollte die Einfaehrung eines SOA Governance Modells Hand in Hand mit der Einfaehrung einer SOA Initiative selbst gehen. Daher dient diese Seminararbeit der Vorstellung der Begriffe SOA und SOA Governance, sowie der konzep- tionellen Definition von SOA Governance Modellen. Weiterhin wird der Nutzen der SOA Governance als Meta-Architektur fuer die SOA typische verteilte Entwicklung dargelegt.
[61]: Markus A. Kuppe and Sebastian Rockel. Model-checking mit spin. December 2009. [ bib | .pdf ]
[62]: Markus A. Kuppe. Multiagenten-simulation und werkzeuge. August 2009. [ bib | http | .pdf ]
[63]: Markus. A. Kuppe and Vitali Amann. Secure service discovery in open networks with slp. July 2009. [ bib | .pdf ]
Abstract Mobile Ad-Hoc networks become increasingly common due to the wide availability of mobile device technology. When such devices enter a network, they want to learn about services offered by other peers or advertise own services. Service discovery protocols have been around to answer this requirement for years. A most prominent and widely adopted one is Service Location Protocol (SLP). However, SLP has not been designed for MANETs, but for trustworhty and reliable networks. Thus the protocol has to undergo a renewal to make it fit for open networks.This paper focuses on the security implications that arise from SLP's usage in open networks and gives a detailed threat analysis. Afterwards security extensions are proposed to address the identified shortcomings.
[64]: Markus. A. Kuppe. Kommunikationstalent eclipse: Das ecf-projekt. Interview at Eclipse Magazin, July 2009. [ bib | .html ]
[65]: Markus A. Kuppe. Distributed osgi - the ecf way. Presentation at Eclipse DemoCamp, Hamburg, Germany, May 2009. [ bib | http | .pdf ]
[66]: Markus A. Kuppe and Scott Lewis. Best practices for distributed osgi services. Presentation at EclipseCon, Santa Clara, CA, USA, March 2009. [ bib | http | .pdf ]
[67]: Markus A. Kuppe and Scott Lewis. Distributed osgi - the ecf way. Tutorial at EclipseCon, Santa Clara, CA, USA, March 2009. [ bib | http | .pdf ]
[68]: Markus A. Kuppe, Jan S. Rellermeyer, and Scott Lewis. Service discovery and remote services with the eclipse communication framework. Presentation at Eclipse Summit Europe, Ludwigsburg, Germany, November 2008. [ bib | http | .pdf ]
[69]: Markus A. Kuppe and Jan S. Rellermeyer. Distributed osgi services with the eclipse communication framework. Presentation at OSGi Community Event, Berlin, Germany, June 2008. [ bib | http | .pdf ]
[70]: Markus A. Kuppe, Jan S. Rellermeyer, and Scott Lewis. Using ecf for lightweight distributed team collaboration. Presentation at EclipseCon, Santa Clara, CA, USA, March 2008. [ bib | http ]
ECF provides a framework for building communications into Eclipse-the-IDE, as well as Eclipse RCP-based and Equinox-based applications. We'll talk about what technical areas to focus on in future work on ECF, and how to get there.
[71]: Markus A. Kuppe and Christian Ernst. An eclipse toolchain for rapid java development using transparent persistence. Presentation at ICOODB, Berlin, Germany, March 2008. [ bib | http | .pdf ]
[72]: Markus A. Kuppe. Component-based software engineering applied to a consolidation using eclipse. Master's thesis, University of Applied Sciences Hamburg, January 2007. B.Sc. thesis. [ bib | .pdf ]
This bachelor thesis deals with the consolidation of a pre-existing software application framed in the context of Component-based Software Engineering (CBSE). The aspects associated with software consolidation and the basic concepts behind CBSE are explained. A process for the conversion of an existing software application in the form of a prototype is then presented. This process covers the discovery of application knowledge in order to effectively extract components and integrate these into a component model. The implemen- tation is accomplished with Eclipse and the OSGi standard, using both in correlation with CBSE. The primary principles guiding this thesis are the presentation of the advantages provided by CBSE and the application of the CBSE paradigm to a consolidation.

This file was generated by bibtex2html 1.99.

Contact