@inproceedings(DBLP:conf/lics/AbdullaDM04,
 author       = "Parosh Aziz Abdulla and Johann Deneux and Pritha Mahata",
 year         = "2004",
 title        = "Multi-Clock Timed Networks",
 booktitle    = "LICS",
 publisher    = "IEEE Computer Society",
 pages        = "345--354",
 doi          = "10.1109/LICS.2004.1319629",
)
@article(DBLP:journals/tcs/AbdullaJ03,
 author       = "Parosh Aziz Abdulla and Bengt Jonsson",
 year         = "2003",
 title        = "Model checking of systems with many identical timed processes",
 journal      = "Theor. Comput. Sci.",
 volume       = "290",
 number       = "1",
 pages        = "241--264",
 doi          = "10.1016/S0304-3975(01)00330-9",
)
@inproceedings(DBLP:conf/lopstr/BandaG08,
 author       = "Gourinath Banda and John P. Gallagher",
 year         = "2008",
 title        = "Analysis of Linear Hybrid Systems in CLP",
 editor       = "Michael Hanus",
 booktitle    = "LOPSTR",
 series       = "Lecture Notes in Computer Science",
 volume       = "5438",
 publisher    = "Springer",
 pages        = "55--70",
 doi          = "10.1007/978-3-642-00515-2\_5",
)
@inproceedings(DBLP:conf/atva/BensalemBSN08,
 author       = "Saddek Bensalem and Marius Bozga and Joseph Sifakis and Thanh-Hung Nguyen",
 year         = "2008",
 title        = "Compositional Verification for Component-Based Systems and Application",
 editor       = "Sung Deok Cha and Jin-Young Choi and Moonzoo Kim and Insup Lee and Mahesh Viswanathan",
 booktitle    = "ATVA",
 series       = "Lecture Notes in Computer Science",
 volume       = "5311",
 publisher    = "Springer",
 pages        = "64--79",
 doi          = "10.1007/978-3-540-88387-6\_7",
)
@inproceedings(DBLP:conf/sas/BjornerMR13,
 author       = "Nikolaj Bj{\o }rner and Kenneth L. McMillan and Andrey Rybalchenko",
 year         = "2013",
 title        = "On Solving Universally Quantified Horn Clauses",
 editor       = "Francesco Logozzo and Manuel F{\"a}hndrich",
 booktitle    = "SAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "7935",
 publisher    = "Springer",
 pages        = "105--125",
 doi          = "10.1007/978-3-642-38856-9\_8",
)
@inproceedings(mcmtexperiments,
 author       = "Alessandro Carioni and Silvio Ghilardi and Silvio Ranise",
 year         = "2010",
 title        = "MCMT in the Land of Parametrized Timed Automata",
 editor       = "Markus Aderhold and Serge Autexier and Heiko Mantel",
 booktitle    = "VERIFY@IJCAR",
 series       = "EPiC Series",
 volume       = "3",
 publisher    = "EasyChair",
 pages        = "47--64",
)
@article(craig1957linear,
 author       = "William Craig",
 year         = "1957",
 title        = "Linear Reasoning. {A} New Form of the {Herbrand-Gentzen} Theorem",
 journal      = "The Journal of Symbolic Logic",
 volume       = "22",
 number       = "3",
 pages        = "250--268",
 doi          = "10.2307/2963593",
)
@article(DBLP:journals/mics/FietzkeW12,
 author       = "Arnaud Fietzke and Christoph Weidenbach",
 year         = "2012",
 title        = "Superposition as a Decision Procedure for Timed Automata",
 journal      = "Mathematics in Computer Science",
 volume       = "6",
 number       = "4",
 pages        = "409--425",
 doi          = "10.1007/s11786-012-0134-5",
)
@article(DBLP:journals/tplp/FioravantiPPS13,
 author       = "Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti and Valerio Senni",
 year         = "2013",
 title        = "Generalization strategies for the verification of infinite state systems",
 journal      = "TPLP",
 volume       = "13",
 number       = "2",
 pages        = "175--199",
 doi          = "10.1017/S1471068411000627",
)
@inproceedings(DBLP:conf/spin/FlanaganQ03,
 author       = "Cormac Flanagan and Shaz Qadeer",
 year         = "2003",
 title        = "Thread-Modular Model Checking",
 editor       = "Thomas Ball and Sriram K. Rajamani",
 booktitle    = "SPIN",
 series       = "Lecture Notes in Computer Science",
 volume       = "2648",
 publisher    = "Springer",
 pages        = "213--224",
 doi          = "10.1007/3-540-44829-2\_14",
)
@inproceedings(GrafSaidi97ConstructionAbstractStateGraphsPVS,
 author       = "Susanne Graf and Hassen Sa\"{\i }di",
 year         = "1997",
 title        = "Construction of Abstract State Graphs with PVS",
 editor       = "Orna Grumberg",
 booktitle    = "CAV",
 series       = "Lecture Notes in Computer Science",
 volume       = "1254",
 publisher    = "Springer",
 pages        = "72--83",
 doi          = "10.1007/3-540-63166-6\_10",
)
@inproceedings(andrey-pldi,
 author       = "Sergey Grebenshchikov and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2012",
 title        = "Synthesizing software verifiers from proof rules",
 editor       = "Jan Vitek and Haibo Lin and Frank Tip",
 booktitle    = "PLDI",
 publisher    = "ACM",
 pages        = "405--416",
 doi          = "10.1145/2254064.2254112",
)
@inproceedings(DBLP:conf/popl/GuptaPR11,
 author       = "Ashutosh Gupta and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2011",
 title        = "Predicate abstraction and refinement for verifying multi-threaded programs",
 editor       = "Thomas Ball and Mooly Sagiv",
 booktitle    = "POPL",
 publisher    = "ACM",
 pages        = "331--344",
 doi          = "10.1145/1926385.1926424",
)
@inproceedings(DBLP:conf/rtss/GuptaP97,
 author       = "Gopal Gupta and Enrico Pontelli",
 year         = "1997",
 title        = "A constraint-based approach for specification and verification of real-time systems",
 booktitle    = "RTSS",
 publisher    = "IEEE Computer Society",
 pages        = "230--239",
 doi          = "10.1109/REAL.1997.641285",
)
@inproceedings(HenzingerETAL04AbstractionsProofs,
 author       = "Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Kenneth L. McMillan",
 year         = "2004",
 title        = "Abstractions from proofs",
 editor       = "Neil D. Jones and Xavier Leroy",
 booktitle    = "POPL",
 publisher    = "ACM",
 pages        = "232--244",
 doi          = "10.1145/964001.964021",
)
@inproceedings(DBLP:conf/sat/HoderB12,
 author       = "Krystof Hoder and Nikolaj Bj{\o }rner",
 year         = "2012",
 title        = "Generalized Property Directed Reachability",
 editor       = "Alessandro Cimatti and Roberto Sebastiani",
 booktitle    = "SAT",
 series       = "Lecture Notes in Computer Science",
 volume       = "7317",
 publisher    = "Springer",
 pages        = "157--171",
 doi          = "10.1007/978-3-642-31612-8\_13",
)
@inproceedings(eldarica-tool,
 author       = "Hossein Hojjat and Filip Konecn{\'y} and Florent Garnier and Radu Iosif and Viktor Kuncak and Philipp R{\"u}mmer",
 year         = "2012",
 title        = "A Verification Toolkit for Numerical Transition Systems - Tool Paper",
 editor       = "Dimitra Giannakopoulou and Dominique M{\'e}ry",
 booktitle    = "FM",
 series       = "Lecture Notes in Computer Science",
 volume       = "7436",
 publisher    = "Springer",
 pages        = "247--251",
 doi          = "10.1007/978-3-642-32759-9\_21",
)
@inproceedings(DBLP:conf/rtss/JaffarSV04,
 author       = "Joxan Jaffar and Andrew E. Santosa and Razvan Voicu",
 year         = "2004",
 title        = "A CLP Proof Method for Timed Automata",
 booktitle    = "RTSS",
 publisher    = "IEEE Computer Society",
 pages        = "175--186",
 doi          = "10.1109/REAL.2004.5",
)
@inproceedings(DBLP:conf/formats/KindermannJN12,
 author       = "Roland Kindermann and Tommi A. Junttila and Ilkka Niemel{\"a}",
 year         = "2012",
 title        = "SMT-Based Induction Methods for Timed Systems",
 editor       = "Marcin Jurdzinski and Dejan Nickovic",
 booktitle    = "FORMATS",
 series       = "Lecture Notes in Computer Science",
 volume       = "7595",
 publisher    = "Springer",
 pages        = "171--187",
 doi          = "10.1007/978-3-642-33365-1\_13",
)
@article(uppaal,
 author       = "Kim Guldstrand Larsen and Paul Pettersson and Wang Yi",
 year         = "1997",
 title        = "UPPAAL in a Nutshell",
 journal      = "STTT",
 volume       = "1",
 number       = "1-2",
 pages        = "134--152",
 doi          = "10.1007/s100090050010",
)
@inproceedings(lopstr07,
 author       = "Mario M{\'e}ndez-Lojo and Jorge A. Navas and Manuel V. Hermenegildo",
 year         = "2007",
 title        = "A Flexible, {(C)LP}-Based Approach to the Analysis of Object-Oriented Programs",
 editor       = "Andy King",
 booktitle    = "LOPSTR",
 series       = "Lecture Notes in Computer Science",
 volume       = "4915",
 publisher    = "Springer",
 pages        = "154--168",
 doi          = "10.1007/978-3-540-78769-3\_11",
)
@article(owicki-gries,
 author       = "Susan S. Owicki and David Gries",
 year         = "1976",
 title        = "An Axiomatic Proof Technique for Parallel Programs I",
 journal      = "Acta Inf.",
 volume       = "6",
 pages        = "319--340",
 doi          = "10.1007/BF00268134",
)
@inproceedings(disjunctive-interpolant,
 author       = "Philipp R{\"u}mmer and Hossein Hojjat and Viktor Kuncak",
 year         = "2013",
 title        = "Disjunctive Interpolants for Horn-Clause Verification",
 editor       = "Natasha Sharygina and Helmut Veith",
 booktitle    = "CAV",
 series       = "Lecture Notes in Computer Science",
 volume       = "8044",
 publisher    = "Springer",
 pages        = "347--363",
 doi          = "10.1007/978-3-642-39799-8\_24",
)
@inproceedings(DBLP:conf/sas/SanchezSSC12,
 author       = "Alejandro S{\'a}nchez and Sriram Sankaranarayanan and C{\'e}sar S{\'a}nchez and Bor-Yuh Evan Chang",
 year         = "2012",
 title        = "Invariant Generation for Parametrized Systems Using Self-reflection - (Extended Version)",
 editor       = "Antoine Min{\'e} and David Schmidt",
 booktitle    = "SAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "7460",
 publisher    = "Springer",
 pages        = "146--163",
 doi          = "10.1007/978-3-642-33125-1\_12",
)
@article(DBLP:journals/csr/WaezDR13,
 author       = "Tawhid Bin Waez and J{\"u}rgen Dingel and Karen Rudie",
 year         = "2013",
 title        = "A survey of timed automata for the development of real-time systems",
 journal      = "Computer Science Review",
 volume       = "9",
 pages        = "1--26",
 doi          = "10.1016/j.cosrev.2013.05.001",
)
@inproceedings(DBLP:conf/forte/YiPD94,
 author       = "Wang Yi and Paul Pettersson and Mats Daniels",
 year         = "1994",
 title        = "Automatic verification of real-time communicating systems by constraint-solving",
 editor       = "Dieter Hogrefe and Stefan Leue",
 booktitle    = "FORTE",
 series       = "IFIP Conference Proceedings",
 volume       = "6",
 publisher    = "Chapman {\&} Hall",
 pages        = "243--258",
)