We list below some key papers related to the development of Spot.
(When adding new entries to this page, please complete the HlinsDatabase with the author homepages and other things that must be turned into hyperlinks.)
1. About Spot
 [duret.04.mascots]

Alexandre DuretLutz and Denis Poitrenaud.
Spot: an extensible model checking library using transitionbased
generalized Büchi automata.
In Proceedings of the 12th IEEE/ACM International Symposium on
Modeling, Analysis, and Simulation of Computer and Telecommunication Systems
(MASCOTS'04), pages 7683, Volendam, The Netherlands, October 2004. IEEE
Computer Society Press.
[ .pdf ]
 [duret.11.vecos]

Alexandre DuretLutz.
LTL translation improvements in Spot.
In Proceedings of the 5th International Workshop on Verification
and Evaluation of Computer and Communication Systems (VECoS'11), Electronic
Workshops in Computing, Tunis, Tunisia, September 2011. British Computer
Society.
[ .pdf ]
See also the SpotPoster.
2. About Algorithms
This list could use an update. In the meantime you may want to check LtlTranslationAlgorithms and EmptinessCheckAlgorithms if you are looking for bibliographical references.
 [baarir.07.acsd]

Souheib Baarir and Alexandre DuretLutz.
Emptiness check of powerset Büchi automata.
In Proceedings of the 7th International Conference on
Application of Concurrency to System Design (ACSD'07), pages 4150. IEEE
Computer Society, July 2007.
[ .pdf ]A special emptiness check for powerset Büchi automata, implemented in Spot.
 [couvreur.05.spin]

JeanMichel Couvreur, Alexandre DuretLutz, and Denis Poitrenaud.
Onthefly emptiness checks for generalized Büchi automata.
In Patrice Godefroid, editor, Proceedings of the 12th
International SPIN Workshop on Model Checking of Software, volume 3639 of
Lecture Notes in Computer Science, pages 143158. ©SpringerVerlag,
August 2005.
[ .pdf ]Comparison of various emptiness check algorithms, all implemented in Spot.
 [couvreur.00.lacim]

JeanMichel Couvreur.
Un point de vue symbolique sur la logique temporelle linéaire.
In Pierre Leroux, editor, Actes du Colloque LaCIM 2000,
volume 27 of Publications du LaCIM, pages 131140. Université du
Québec à Montréal, August 2000.
[ .pdf ]This paper describes a LTLtoBüchi translation algorithm available in Spot as ltl_to_tgba_lacim(). The automata produced are not really small. However they are really fast to build, and can be represented compactly using BDDs.
 [couvreur.99.fm]

JeanMichel Couvreur.
Onthefly verification of temporal logic.
In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors,
Proceedings of the World Congress on Formal Methods in the Development of
Computing Systems (FM'99), volume 1708 of Lecture Notes in Computer Science, pages 253271, Toulouse, France, September 1999. ©SpringerVerlag.
[ .pdf ]Work started on Spot to implement the algorithms introduced in this paper. The LTLtoBüchi translation algorithm is available in Spot as ltl_to_tgba_fm(). The emptinesscheck with generalized acceptance conditions is implemented by the emptiness_check class.
 [minato.92.sasimi]

Shinichi Minato.
Fast generation of irredundant sumofproducts forms from binary
decision diagrams.
In Proceedings of the third Synthesis and Simulation Meeting and
International Interchange workshop (SASIMI'92), pages 6473, Kobe, Japan,
April 1992.
[ .pdf ]The LTL translator algorithm from [couvreur.99.fm] requires some prime impliquant computation. We use the MinatoMorreale algorithm.
 [godefroid.93.pstv]

Patrice Godefroid and Gerard J. Holzmann.
On the verification of temporal properties.
In André A. S. Danthine, Guy Leduc, and Pierre Wolper, editors,
Proceedings of the 13th IFIP TC6/WG6.1 International Symposium on
Protocol Specification, Testing, and Verification (PSTV'93), volume C16 of
IFIP Transactions, pages 109124, Liege, Belgium, May 1993.
NorthHolland.
[ .pdf ]The magic search is available in Spot as a magic_search class.
 [giannakopoulou.02.forte]

Dimitra Giannakopoulou and Flavio Lerda.
From states to transitions: Improving translation of LTL formulae
to Büchi automata.
In Doron A. Peled and Moshe Y. Vardi, editors, Proceedings of
the 22nd IFIP WG 6.1 International Conference on Formal Techniques for
Networked and Distributed Systems (FORTE'02), volume 2529 of Lecture Notes in Computer Science, pages 308326, Houston, Texas, November 2002.
©SpringerVerlag.
[ .pdf ]This papers introduces Transitionsbased Generalized Büchi automata (TGBA) and explains how they are smaller than the usual statebased Büchi automata. TGBAs were already used earlier in [couvreur.99.fm] and [couvreur.00.lacim] but this paper coined the acronym TGBA which we are using in Spot. Spot's tgba is an abstract class with many possible implementations. Its interface really is the heart of the library.
 [sebastiani.03.charme]

Roberto Sebastiani and Stefano Tonetta.
more deterministic vs. smaller büchi automata for efficient
ltl model checking.
In G. Goos, J. Hartmanis, and J. van Leeuwen, editors,
Proceedings for the 12th Advanced Research Working Conference on Correct
Hardware Design and Verification Methods (CHARME'03), volume 2860 of
Lecture Notes in Computer Science, pages 126140. ©SpringerVerlag, October
2003.
[ .ps ]This paper introduces two optimizations which we have implemented into Couvreur's [couvreur.99.fm] algorithm to obtain more deterministic automata. These are the semantic branching (which is called exprop inside Spot and optimize determinism on the online LTLtoTGBA translator) and the branching postponement.