@inproceedings(signal,
 author       = "Pascalin Amagb{\'e}gnon and Lo\"{\i }c Besnard and Paul Le Guernic",
 year         = "1995",
 title        = "Implementation of the Data-Flow Synchronous Language SIGNAL",
 booktitle    = "PLDI",
 pages        = "163--173",
 url          = "http://doi.acm.org/10.1145/207110.207134",
)
@incollection(Benveniste91thesynchronous,
 author       = "Albert Benveniste and G{\'e}rard Berry",
 year         = "2002",
 title        = "The Synchronous Approach to Reactive and Real-time Systems",
 editor       = "Giovanni De Micheli and Rolf Ernst and Wayne Wolf",
 booktitle    = "Readings in Hardware/Software Co-design",
 publisher    = "Kluwer Academic Publishers",
 address      = "Norwell, MA, USA",
 pages        = "147--159",
 url          = "http://doi.acm.org/10.1016/B978-155860702-6/50013-2",
)
@article(esterel,
 author       = "G{\'e}rard Berry and Georges Gonthier",
 year         = "1992",
 title        = "The Esterel Synchronous Programming Language:\newline Design, Semantics, Implementation",
 journal      = "Sci. Comput. Program.",
 volume       = "19",
 number       = "2",
 pages        = "87--152",
 url          = "http://dx.doi.org/10.1016/0167-6423(92)90005-V",
)
@inproceedings(DBLP:conf/popl/CaspiPHP87,
 author       = "Paul Caspi and Daniel Pilaud and Nicolas Halbwachs and John Plaice",
 year         = "1987",
 title        = "Lustre: A Declarative Language for Programming Synchronous Systems",
 booktitle    = "POPL",
 pages        = "178--188",
 url          = "http://doi.acm.org/10.1145/41625.41641",
)
@inproceedings(cegar,
 author       = "Edmund M. Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith",
 year         = "2000",
 title        = "Counterexample-Guided Abstraction Refinement",
 booktitle    = "CAV",
 pages        = "154--169",
 url          = "http://dx.doi.org/10.1007/10722167_15",
)
@inproceedings(GarocheKT13,
 author       = "Pierre-Lo\"{\i }c Garoche and Temesghen Kahsai and Cesare Tinelli",
 year         = "2013",
 title        = "Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers",
 booktitle    = "NASA Formal Methods",
 pages        = "139--154",
 url          = "http://dx.doi.org/10.1007/978-3-642-38088-4_10",
)
@inproceedings(GuptaPR11b,
 author       = "Ashutosh Gupta and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2011",
 title        = "Solving Recursion-Free Horn Clauses over LI+UIF",
 booktitle    = "APLAS",
 pages        = "188--203",
 url          = "http://dx.doi.org/10.1007/978-3-642-25318-8_16",
)
@inproceedings(GuptaPR11,
 author       = "Ashutosh Gupta and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2011",
 title        = "Threader: A Constraint-Based Verifier for Multi-threaded Programs",
 booktitle    = "CAV",
 pages        = "412--417",
 url          = "http://dx.doi.org/10.1007/978-3-642-22110-1_32",
)
@inproceedings(pdr,
 author       = "Krystof Hoder and Nikolaj Bj{\o }rner",
 year         = "2012",
 title        = "Generalized Property Directed Reachability",
 booktitle    = "SAT",
 pages        = "157--171",
 url          = "http://dx.doi.org/10.1007/978-3-642-31612-8_13",
)
@inproceedings(KahGT-NFM-11,
 author       = "Temesghen Kahsai and Yeting Ge and Cesare Tinelli",
 year         = "2011",
 title        = "Instantiation-Based Invariant Discovery",
 booktitle    = "NASA Formal Methods",
 pages        = "192--206",
 url          = "http://dx.doi.org/10.1007/978-3-642-20398-5_15",
)
@inproceedings(Rushby:2012,
 author       = "John Rushby",
 year         = "2014",
 title        = "The Versatile Synchronous Observer",
 booktitle    = "Specification, Algebra, and Software",
 pages        = "110--128",
 url          = "http://dx.doi.org/10.1007/978-3-642-54624-2_6",
)