@mastersthesis{Kuppe2017,
title = {A Verified and Scalable Hash Table for the TLC Model Checker
Towards an Order of Magnitude Speedup},
author = {Kuppe, Markus A.},
school = {University of Hamburg},
year = {2017},
note = {Grade 1.0},
abstract = {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.},
owner = {markus},
pdf = {http://www.lemmster.de/talks/MSc_MarkusAKuppe_1497363471.pdf},
timestamp = {2017.06.15}
}
@misc{Kuppe2018a,
author = {Kuppe, Markus A.},
title = {Mit TLA+ zum korrekten Parallelprogramm},
howpublished = {parallel 2018},
month = {July},
year = {2018},
abstract = {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.},
owner = {markus},
timestamp = {2019-05-13},
url = {http://www.lemmster.de/talks/Mit_TLAPlus_zum_korekten_Parallelprogram_-_Markus_Alexader_Kuppe.pdf}
}
@misc{Kuppe2013,
title = {Discover Remote Services},
author = {Kuppe, Markus A.},
howpublished = {Eclipse Democamp Hamburg},
month = {November},
year = {2013},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Discover_Remote_Services_-_Democamp_HH_2013_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2013.11.27},
url = {http://wiki.eclipse.org/Eclipse_DemoCamps_November_2013/Hamburg}
}
@misc{Kuppe2012,
title = {Current state of distributed TLC},
author = {Kuppe, Markus. A.},
howpublished = {International Workshop on the TLA+ Method and Tools},
month = {August},
year = {2012},
owner = {markus},
pdf = {http://www.lemmster.de/talks/CurrentStateDistributedTLC_MarkusAKuppe.pdf},
timestamp = {2012.09.14},
url = {http://tla2012.loria.fr/index.html, http://www.lemmster.de/uploads/CurrentStateDistributedTLC_MarkusAKuppe.pdf}
}
@unpublished{Kuppe2010,
title = {SOA Governance},
author = {Kuppe, Markus. A.},
month = {February},
year = {2010},
abstract = {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.},
comment = {http://vsis-www.informatik.uni-hamburg.de/teaching/termine.php/195},
owner = {markus},
pdf = {http://www.lemmster.de/talks/SOA_Governance_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.14}
}
@misc{Kuppe2010a,
title = {Entwicklung verteilter Eclipse RCP \& OSGi Anwendungen mit dem Eclipse Communication Framework},
author = {Kuppe, Markus A.},
howpublished = {Full day tutorial at University of Hamburg Summerschool},
month = {October},
year = {2010},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Entwicklung_verteilter_Eclipse_OSGi_Anwendungen_mit_ECF_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.15},
url = {http://github.com/lemmy/org.eclipse.ecf.winterschool/raw/master/org.eclipse.ecf.winterschool/EclipseCommunicationFramework.odp}
}
@misc{Kuppe2009,
title = {Distributed OSGi - The ECF way},
author = {Kuppe, Markus A.},
howpublished = {Presentation at Eclipse DemoCamp, Hamburg, Germany},
month = {May},
year = {2009},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Distributed_OSGi_-_The_ECF_way-DemoCamp_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.14},
url = {http://wiki.eclipse.org/Eclipse_DemoCamps_Galileo_2009/Hamburg}
}
@misc{Kuppe2009a,
title = {Kommunikationstalent Eclipse: Das ECF-Projekt},
author = {Kuppe, Markus. A.},
howpublished = {Interview at Eclipse Magazin},
month = {July},
year = {2009},
owner = {markus},
timestamp = {2012.09.14},
url = {http://entwickler.de/zonen/portale/psecom,id,101,online,2403.html}
}
@unpublished{Kuppe2009b,
title = {Multiagenten-Simulation und Werkzeuge},
author = {Kuppe, Markus A.},
month = {August},
year = {2009},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Multiagenten-Simulation_und_Werkzeuge-Markus_A_Kuppe.pdf},
timestamp = {2012.09.14},
url = {http://vsis-www.informatik.uni-hamburg.de/teaching/termine.php/179}
}
@mastersthesis{Kuppe2007,
title = {Component-based software engineering applied to a consolidation using Eclipse},
author = {Kuppe, Markus A.},
school = {University of Applied Sciences Hamburg},
year = {2007},
month = {January},
note = {B.Sc. thesis},
abstract = {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.},
owner = {markus},
pdf = {http://www.lemmster.de/hawhhcsbsc.pdf},
timestamp = {2012.09.14}
}
@unpublished{Kuppe2009c,
title = {Secure service discovery in open networks with SLP},
author = {Kuppe, Markus. A. and Amann, Vitali},
month = {July},
year = {2009},
abstract = {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.},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Secure_service_discovery_in_open_networks_with_SLP_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.14}
}
@misc{Kuppe2008,
title = {An Eclipse Toolchain for rapid Java development using transparent persistence},
author = {Kuppe, Markus A. and Ernst, Christian},
howpublished = {Presentation at ICOODB, Berlin, Germany},
month = {March},
year = {2008},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Eclipse_Toolchain_for_rapid_Java_development_using_transparent_persistence_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.14},
url = {http://projekt.tfh-berlin.de/icoodb/icoodb-2008/}
}
@misc{Kuppe2013a,
title = {Discover Remote OSGi Services},
author = {Kuppe, Markus A. and Jongman, Wim},
howpublished = {Presentation at EclipseCon Europe 2013, Ludwigsburg, Germany},
month = {October},
year = {2013},
abstract = {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.},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Discover_Remote_OSGi_Services_-_Markus_Alexander_Kuppe-Wim_Jongman.pdf},
timestamp = {2013.11.01},
url = {https://www.eclipsecon.org/europe2013/discover-remote-osgi-services}
}
@misc{Kuppe2010b,
title = {Fun with Remote Services},
author = {Kuppe, Markus A. and Jongman, Wim},
howpublished = {Presentation at Eclipse Summit Europe},
month = {November},
year = {2010},
abstract = {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"},
owner = {markus},
timestamp = {2012.09.14},
url = {https://www.eclipsecon.org/submissions/ese2010/view_talk.php?id=1916}
}
@misc{Kuppe2009d,
title = {Distributed OSGi - The ECF way},
author = {Kuppe, Markus A. and Lewis, Scott},
howpublished = {Tutorial at EclipseCon, Santa Clara, CA, USA},
month = {March},
year = {2009},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Distributed_OSGi_-_The_ECF_way_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.14},
url = {http://www.eclipsecon.org/2009/sessions?id=618}
}
@misc{Kuppe2009e,
title = {Best Practices for Distributed OSGi Services},
author = {Kuppe, Markus A. and Lewis, Scott},
howpublished = {Presentation at EclipseCon, Santa Clara, CA, USA},
month = {March},
year = {2009},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Best_Practices_with_Distributed_OSGi_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.14},
url = {http://www.eclipsecon.org/2009/sessions?id=757}
}
@misc{Kuppe2008a,
title = {Distributed OSGi Services with the Eclipse Communication Framework},
author = {Kuppe, Markus A. and Rellermeyer, Jan S.},
howpublished = {Presentation at OSGi Community Event, Berlin, Germany},
month = {June},
year = {2008},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Distributed_OSGi_Services_with_the_Eclipse_Communication_Framework_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.14},
url = {http://www.osgi.org/CommunityEvent2008/Program}
}
@misc{Kuppe2008b,
title = {Service Discovery and Remote Services with the Eclipse Communication Framework},
author = {Kuppe, Markus A. and Rellermeyer, Jan S. and Lewis, Scott},
howpublished = {Presentation at Eclipse Summit Europe, Ludwigsburg, Germany},
month = {November},
year = {2008},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Service_Discovery_and_Remote_Services_with_the_Eclipse_Communication_Framework_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.14},
url = {http://www.eclipsecon.org/summiteurope2008/sessions?id=89}
}
@misc{Kuppe2008c,
title = {Using ECF for Lightweight Distributed Team Collaboration},
author = {Kuppe, Markus A. and Rellermeyer, Jan S. and Lewis, Scott},
howpublished = {Presentation at EclipseCon, Santa Clara, CA, USA},
month = {March},
year = {2008},
abstract = {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.},
owner = {markus},
timestamp = {2012.09.14},
url = {http://www.eclipsecon.org/2008/index.php?page=sub&id=610}
}
@unpublished{Kuppe2009f,
title = {Model-Checking mit SPIN},
author = {Kuppe, Markus A. and Rockel, Sebastian},
month = {December},
year = {2009},
comment = {Seminar Logik und Semantik von Programmen (FGI 3)},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Model-Checking_mit_SPIN_-_Markus_Alexander_Kuppe.pdf},
timestamp = {2012.09.14}
}
@misc{Vogel2013,
title = {Become an Eclipse Committer in 20 min and fork the Eclipse IDE},
author = {Vogel, Lars and Kuppe, Markus A.},
howpublished = {Presentation at EclipseCon Europe 2013, Ludwigsburg, Germany},
month = {October},
year = {2013},
abstract = {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.},
owner = {markus},
pdf = {http://www.lemmster.de/talks/Become_Committer_in_20_minutes_-_Markus_Alexander_Kuppe-Lars_Vogel.pdf},
timestamp = {2013.11.01},
url = {https://www.eclipsecon.org/europe2013/become-eclipse-committer-20-min-and-fork-eclipse-ide}
}
@misc{Kuppe2014,
author = {Kuppe, Markus A.},
title = {Distributed TLC},
howpublished = {TLA+ Community Event (co-located with ABZ 2014)},
month = {June},
year = {2014},
note = {http://tla2014.loria.fr/},
owner = {markus},
timestamp = {2014.06.08},
url = {http://www.lemmster.de/talks/DistributedTLC_MarkusAKuppe.pdf}
}
@misc{Kuppe2018d,
author = {Kuppe, Markus A.},
title = {State Space Explosion or: How To Fight An Uphill Battle (Tutorial)},
howpublished = {TLA+ Community Event (co-located with FM 2018)},
month = {July},
year = {2018},
note = {http://tla2018.loria.fr/},
owner = {markus},
timestamp = {2014.06.08},
url = {https://www.youtube.com/watch?v=zGIK2p6csAo&list=PLWLcqZLzY8u_3mDg2cHmduA5wl4J6hNX2&index=6}
}
@misc{Kuppe2018c,
author = {Kuppe, Markus A.},
title = {Weeks of debugging can save you hours of TLA+},
howpublished = {Java User Group hamburg},
month = {June},
year = {2018},
owner = {markus},
timestamp = {2019-05-13},
url = {https://www.meetup.com/jug-hamburg/events/250933411/}
}
@misc{Kuppe2019,
author = {Kuppe, Markus A.},
title = {Debuggable Design with TLA+},
howpublished = {Hyperscale Verification},
month = {March},
year = {2019},
owner = {markus},
timestamp = {2019-05-13},
url = {http://www.lemmster.de/talks/Hyperscale_Verification_-_Markus_Alexander_Kuppe.pdf}
}
@misc{Kuppe2018b,
author = {Kuppe, Markus A.},
title = {Large Scale Model Checking 101},
howpublished = {TLA+ Workshop: Presentations},
month = {April},
year = {2018},
owner = {markus},
timestamp = {2019-05-13},
url = {https://resnet.microsoft.com/video/40879}
}
@misc{Kuppe2018e,
author = {Kuppe, Markus A.},
title = {Let TLA+ RiSE},
howpublished = {RiSE group all-hands meeting},
month = {August},
year = {2018},
owner = {markus},
timestamp = {2019-05-13},
url = {http://www.lemmster.de/talks/Let_TLA_RiSE_-_Markus_Alexander_Kuppe.pdf}
}
@misc{Kuppe2019a,
author = {Kuppe, Markus A.},
title = {The TLA+ Toolbox},
howpublished = {F-IDE 2019},
month = {October},
year = {2019},
owner = {markus},
timestamp = {2019-05-13},
url = {https://easychair.org/smart-slide/slide/wvZm#}
}
@misc{Kuppe2019b,
author = {Kuppe, Markus A.},
title = {#70 Intro To TLA+ \& Formal Smart Contract Design Specification},
howpublished = {Let's Talk ETC! Podcast},
month = {March},
year = {2019},
url = {https://youtu.be/z-DyBFQzSVk?list=PLWLcqZLzY8u_ix-R-pikzj-4qTjJbqAil}
}
@misc{Kuppe2019c,
author = {Kuppe, Markus A.},
title = {TLA+ meets Azure Bootcamp},
howpublished = {Microsoft Internal (BootCamp)},
month = {November},
year = {2019}
}
@article{Kuppe_2019,
author = {Kuppe, Markus Alexander and Lamport, Leslie and Ricketts, Daniel},
title = {The TLA+ Toolbox},
journal = {Electronic Proceedings in Theoretical Computer Science},
year = {2019},
volume = {310},
pages = {50–62},
month = {December},
issn = {2075-2180},
doi = {10.4204/eptcs.310.6},
publisher = {Open Publishing Association},
url = {http://dx.doi.org/10.4204/EPTCS.310.6}
}
@misc{Kuppe2019d,
author = {Kuppe, Markus A.},
title = {TLA+ meets Java@Microsoft},
howpublished = {Microsoft Internal (BrownBag)},
month = {December},
year = {2019},
url = {https://msit.microsoftstream.com/video/d4fe1577-be1f-4246-b256-24f29a24de0e}
}
@misc{Kuppe2020,
author = {Kuppe, Markus A.},
title = {MSR Central Engineering Pitch Tank},
howpublished = {Microsoft Internal},
month = {January},
year = {2020}
}
@misc{Kuppe2020b,
author = {Kuppe, Markus A.},
title = {TLA+ meets Microsoft Avere},
howpublished = {Microsoft Internal (BrownBag)},
month = {February},
year = {2020},
url = {https://msit.microsoftstream.com/video/6fa6e119-5923-4b76-896a-3b12eb0c01d1}
}
@misc{Kuppe2020c,
author = {Kuppe, Markus A.},
title = {TLA+: The Tools, The Language, The Application},
howpublished = {Invited Talk at University of Buffalo, Host: Prof Murat Demirbas},
month = {February},
year = {2020}
}
@misc{Kuppe2020d,
author = {Kuppe, Markus A.},
title = {TLA+: The Tools, The Language, The Application},
howpublished = {Invited Talk at Penn State University, Host: Prof George Kesidis},
month = {February},
year = {2020}
}
@misc{Kuppe2020e,
author = {Kuppe, Markus A.},
title = {TLA+ meets MRS Healthcare},
howpublished = {Microsoft Internal (BrownBag)},
month = {June},
year = {2020},
url = {https://msit.microsoftstream.com/video/8855a1ff-0400-a521-7bf6-f1eaba41ede9}
}
@misc{Kuppe2019f,
author = {Kuppe, Markus A.},
title = {TLA+ meets Azure Bootcamp},
howpublished = {Microsoft Internal (Bootcamp)},
month = {July},
year = {2020},
url = {https://msit.microsoftstream.com/video/9515a4ff-0400-a521-77ff-f1eacc4362b7}
}
@misc{Kuppe2019g,
author = {Kuppe, Markus A.},
title = {TLA+ meets Azure Bootcamp},
howpublished = {Microsoft Internal (BrownBag)},
month = {July},
year = {2020}
}
@misc{Kuppe2019h,
author = {Kuppe, Markus A.},
title = {Weeks of debugging can save you hours of TLA+},
howpublished = {Usenix SRE Con West},
month = {March},
year = {2020},
note = {Talk accepted - Conference cancelled due to Covid19}
}
@misc{Kuppe2019i,
author = {Kuppe, Markus A.},
title = {Weeks of debugging can save you hours of TLA+},
howpublished = {CodeStock},
month = {April},
year = {2020},
note = {Talk accepted - Conference cancelled due to Covid19}
}
@misc{Kuppe2019j,
author = {Kuppe, Markus A.},
title = {TLA+ at TechFest},
howpublished = {Microsoft Internal (TechFest)},
month = {April},
year = {2020},
note = {Accepted - Cancelled due to Covid19},
url = {https://msit.microsoftstream.com/video/d61aa07c-2992-4075-8306-35d21faf9ad9}
}
@misc{Kuppe2020k,
author = {Kuppe, Markus A.},
title = {TLA+ meets Azure Bootcamp},
howpublished = {Microsoft Internal (BrownBag)},
month = {August},
year = {2020}
}
@misc{Kuppe2020l,
author = {Kuppe, Markus A.},
title = {TLA+ meets Azure Bootcamp},
howpublished = {Microsoft Internal (BrownBag)},
month = {September},
year = {2020}
}
@misc{Kuppe2020m,
author = {Kuppe, Markus A.},
title = {TLA+ meets Azure Bootcamp},
howpublished = {Microsoft Internal (BrownBag)},
month = {November},
year = {2020}
}
@misc{Kuppe2020n,
author = {Lamport, Leslie and Kuppe, Markus A.},
title = {TLA+ : Viewed From 40,000 Feet and Ground Level},
howpublished = {Microsoft Internal (Speaker Series)},
month = {October},
year = {2020}
}
@misc{Kuppe2020o,
author = {Kuppe, Markus A.},
title = {TLA+},
howpublished = {Microsoft Internal (RiSE all-hands)},
month = {December},
year = {2020}
}
@inproceedings{262190,
author = {Markus A. Kuppe},
title = {Weeks of Debugging Can Save You Hours of TLA+},
booktitle = {SREcon20 Americas (SREcon20 Americas)},
year = {2020},
month = dec,
publisher = {{USENIX} Association},
url = {https://www.usenix.org/conference/srecon20americas/presentation/kuppe}
}
@misc{Kuppe2021a,
author = {Kuppe, Markus A.},
month = {June},
title = {Workshop: TLA+ in Action},
year = {2021},
url = {https://2021.hydraconf.com/2021/msk/talks/5oob1c0bvepx2cgfm8botq/}
}
@misc{Kuppe2021b,
author = {Lamport, Leslie and Kuppe, Markus A.},
month = {August},
title = {TLA+ : Viewed From 40,000 Feet and Ground Level},
howpublished = {LinkedIn Internal (Tech Talk Series)},
year = {2021}
}
@misc{Kuppe2021c,
author = {Kuppe, Markus A.},
month = {September},
title = {Workshop: TLA+ in Action},
howpublished = {Strange Loop Workshop},
year = {2021}
}
@misc{Kuppe2021d,
author = {Kuppe, Markus A.},
month = {September},
title = {Workshop: TLA+ in Action},
howpublished = {Strange Loop Workshop},
year = {2021}
}
@misc{Kuppe2022a,
author = {Kuppe, Markus A.},
month = {February},
title = {Shift-Shift-Left Design},
howpublished = {Microsoft Internal (Cloud Reliability RIA all-hands)},
year = {2022}
}
@misc{Kuppe2022b,
author = {Kuppe, Markus A.},
month = {January},
title = {Weeks Of Debugging Can Save You Hours of TLA+},
howpublished = {Detroit Tech Watch Meetup},
year = {2022},
url = {https://www.youtube.com/watch?v=4mzD-DIRpKY}
}
@misc{Kuppe2022c,
author = {Kuppe, Markus A.},
month = {January},
title = {Rise4Fun},
howpublished = {Microsoft Internal (RiSE all-hands)},
year = {2022}
}
@misc{Kuppe2022d,
author = {Kuppe, Markus A.},
month = {February},
title = {Rise4Fun & Profit - Github Codespaces & VSCode},
howpublished = {Microsoft Internal (RiSE all-hands)},
year = {2022}
}
@misc{Kuppe2022e,
author = {Kuppe, Markus A.},
month = {March},
title = {Weeks of debugging can save you hours of TLA+},
howpublished = {Microsoft Internal (CODE Conf)},
year = {2022}
}
@misc{Kuppe2022f,
author = {Kuppe, Markus A.},
month = {April},
title = {TLC Changelog},
howpublished = {Microsoft Internal (Brown Bag)},
year = {2022}
}
@misc{Kuppe2022g,
author = {Kuppe, Markus A.},
month = {May},
title = {Weeks of debugging can save you hours of TLA+},
howpublished = {Microsoft Internal (Cloud Talks)},
year = {2022}
}
@misc{Kuppe2022h,
author = {Kuppe, Markus A.},
month = {May},
title = {Cloud Reliability::TLA+},
howpublished = {Microsoft Internal (RiSE all-hands)},
year = {2022}
}
@misc{Kuppe2022i,
author = {Kuppe, Markus A.},
month = {May},
title = {Let's shift-shift left: How modeling can help software engineering},
howpublished = {Microsoft Internal (Storytelling Workshop)},
url = {https://www.youtube.com/watch?v=yJdY-RNlpuE},
year = {2022}
}
@misc{Kuppe2022j,
author = {Kuppe, Markus A.},
month = {February},
title = {Weeks of debugging can save you hours of TLA+ (Extended Version)},
howpublished = {Distributed Systems Meetup Pune},
url = {https://www.youtube.com/watch?v=uPNFcTAgw3E},
year = {2022}
}
@misc{Kuppe2022k,
author = {Kuppe, Markus A.},
month = {June},
title = {TLA+ in 5 minutes},
howpublished = {Microsoft Internal (RiSE all-hands)},
year = {2022}
}
@misc{Kuppe2022l,
author = {Kuppe, Markus A.},
month = {June},
title = {TLA+: The Tools, The Language, The Application},
howpublished = {Invited Talk at University of British Columbia (UBC), Canada},
year = {2022}
}
@misc{Kuppe2022m,
author = {Rowe, Joshua and Kuppe, Markus A. and Hackett, Finn},
month = {July},
title = {Understanding Inconsistency in Azure Cosmos DB with TLA+},
howpublished = {Microsoft Internal (Cloud Reliability RIA all-hands)},
year = {2022}
}
@misc{Kuppe2022n,
author = {Kuppe, Markus A.},
howpublished = {MCH2022},
month = {July},
title = {{W}orkshop: {TLA+} in {A}ction - Blocking {Q}ueue},
year = {2022},
url = {https://program.mch2022.org/mch2022/talk/9N7CTV/}
}
@misc{Kuppe2022o,
author = {Kuppe, Markus A.},
howpublished = {Distributed Systems Meetup Bangaluru},
month = {August},
title = {{W}orkshop: {TLA+} in {A}ction - Blocking {Q}ueue},
year = {2022},
url = {https://www.youtube.com/watch?v=lsgDQhMC19o}
}
@article{Kuppe2022,
author = {Kuppe, Markus A.},
journal = {F-IDE 2022},
title = {{T}he {TLA+} {D}ebugger},
year = {2022},
month = sep,
pages = {To Appear},
comment = {https://www.youtube.com/watch?v=DsfbdsE4hJ0},
url = {https://drive.google.com/file/d/1NtT21oaU7PlZxCMahP5XD5gEwrYOPAAO/view}
}
@article{Merz2022,
author = {Merz, Stephan and Konnov, Igor and Kuppe, Markus A.},
journal = {SpecifyThis at ISoLA},
title = {{S}pecification and {V}erification wth the {TLA+} {T}rifecta: {TLC}, {Apalache}, and {TLAPS}},
year = {2022},
month = nov,
pages = {To Appear}
}
@article{Rowe2023,
author = {Rowe, Joshua and Kuppe, Markus A. and Hackett, Finn},
title = {{U}nderstanding {I}nconsistency in {A}zure {C}osmos{DB} with {TLA+}},
year = {2023},
pages = {Submitted}
}
@misc{Kuppe2022p,
author = {Kuppe, Markus A.},
howpublished = {Tutorial Series of the FME Teaching Committee},
month = dec,
title = {{T}eaching {TLA+} in {I}ndustry},
year = {2022},
url = {https://fme-teaching.github.io}
}
@misc{Valightly2022,
author = {Valightly, Jack and Kuppe, Markus A.},
howpublished = {TLA+ Conference},
month = sep,
title = {{O}btaining statistical propertiesby simulating specs with {TLC}},
year = {2022},
url = {http://conf.tlapl.us/2022/}
}
This file was generated by bibtex2html 1.99.