@inproceedings(AlurH91,
 author       = "Rajeev Alur and Thomas~A. Henzinger",
 year         = "1991",
 title        = "Logics and Models of Real Time: A Survey",
 booktitle    = "REX Workshop",
 pages        = "74--106",
 doi          = "10.1007/BFb0031988",
)
@inproceedings(BiereCCFZ99,
 author       = "Armin Biere and Alessandro Cimatti and Edmund~M. Clarke and Yunshan Zhu",
 year         = "1999",
 title        = "Symbolic Model Checking without BDDs",
 booktitle    = "TACAS",
 pages        = "193--207",
 doi          = "10.1007/3-540-49059-0\_14",
)
@inproceedings(BiereCZ99,
 author       = "Armin Biere and Edmund~M. Clarke and Yunshan Zhu",
 title        = "Multiple State and Single State Tableaux for Combining Local and Global Model Checking",
 doi          = "10.1007/3-540-48092-7\_8",
)
@inproceedings(BroersenDDM04,
 author       = "Jan Broersen and Frank Dignum and Virginia Dignum and John-Jules~Ch. Meyer",
 year         = "2004",
 title        = "Designing a Deontic Logic of Deadlines",
 booktitle    = "DEON",
 doi          = "10.1007/978-3-540-25927-5\_5",
)
@article(BurchCMDH92,
 author       = "Jerry~R. Burch and all.",
 year         = "1992",
 title        = "Symbolic Model Checking: $10^{20}$ States and Beyond",
 journal      = "Inf. Comput.",
 volume       = "98",
 number       = "2",
 pages        = "142--170",
 doi          = "10.1016/0890-5401(92)90017-A",
)
@inproceedings(CimattiRST07,
 author       = "A.~Cimatti and M.~Roveri and V.~Schuppan and S.~Tonetta",
 year         = "2007",
 title        = "Boolean Abstraction for Temporal Logic Satisfiability",
 booktitle    = "CAV",
 pages        = "532--546",
 doi          = "10.1007/978-3-540-73368-3\_53",
)
@inproceedings(DamaggioDV11,
 author       = "Elio Damaggio and Alin Deutsch and Victor Vianu",
 year         = "2011",
 title        = "Artifact systems with data dependencies and arithmetic",
 booktitle    = "ICDT",
 pages        = "66--77",
 doi          = "10.1145/1938551.1938563",
)
@article(Davis1962,
 author       = "Martin Davis and George Logemann and Donald~W. Loveland",
 year         = "1962",
 title        = "A machine program for theorem-proving",
 journal      = "Commun. ACM",
 volume       = "5",
 number       = "7",
 pages        = "394--397",
 doi          = "10.1145/368273.368557",
)
@article(Emerson,
 author       = "E.~Emerson",
 year         = "1990",
 title        = "Temporal and Modal Logic",
 journal      = "HTCS, Volume B: Formal Models and Sematics (B)",
)
@inproceedings(FenechPS09,
 author       = "Stephen Fenech and Gordon~J. Pace and Gerardo Schneider",
 year         = "2009",
 title        = "Automatic Conflict Detection on Contracts",
 booktitle    = "ICTAC",
 pages        = "200--214",
 doi          = "10.1007/978-3-642-03466-4\_13",
)
@article(FischerL79,
 author       = "Michael~J. Fischer and Richard~E. Ladner",
 year         = "1979",
 title        = "Propositional Dynamic Logic of Regular Programs",
 journal      = "J. Comput. Syst. Sci.",
 volume       = "18",
 number       = "2",
 pages        = "194--211",
 doi          = "10.1016/0022-0000(79)90046-1",
)
@inproceedings(Fisher91,
 author       = "Michael Fisher",
 year         = "1991",
 title        = "A Resolution Method for Temporal Logic",
 booktitle    = "IJCAI",
 pages        = "99--104",
)
@inproceedings(GanaiGA05,
 author       = "Malay~K. Ganai and Aarti Gupta and Pranav Ashar",
 year         = "2005",
 title        = "Beyond safety: customized SAT-based model checking",
 booktitle    = "DAC",
 pages        = "738--743",
 doi          = "10.1145/1065579.1065773",
)
@inproceedings(GerthPVW95,
 author       = "Rob Gerth and Doron Peled and Moshe~Y. Vardi and Pierre Wolper",
 year         = "1995",
 title        = "Simple on-the-fly automatic verification of linear temporal logic",
 booktitle    = "PSTV",
 pages        = "3--18",
)
@inproceedings(GhoseK07,
 author       = "Aditya Ghose and George Koliadis",
 year         = "2007",
 title        = "Auditing Business Process Compliance",
 booktitle    = "ICSOC",
 pages        = "169--180",
 doi          = "10.1007/978-3-540-74974-5\_14",
)
@inproceedings(GiblinLMPZ05,
 author       = "C.~Giblin and A.~Liu and S.~M{\"u}ller and B.~Pfitzmann",
 year         = "2005",
 title        = "Regulations Expressed As Logical Models (REALM)",
 booktitle    = "JURIX",
 pages        = "37--48",
)
@inproceedings(HeljankoJL05,
 author       = "Keijo Heljanko and Tommi~A. Junttila and Timo Latvala",
 year         = "2005",
 title        = "Incremental and Complete Bounded Model Checking for Full PLTL",
 booktitle    = "CAV",
 pages        = "98--111",
 doi          = "10.1007/11513988\_10",
)
@article(JussilaB07,
 author       = "Toni Jussila and Armin Biere",
 year         = "2007",
 title        = "Compressing BMC Encodings with QBF",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "174",
 number       = "3",
 pages        = "45--56",
 doi          = "10.1016/j.entcs.2006.12.022",
)
@inproceedings(KestenMMP93,
 author       = "Y.~Kesten and Z.~Manna and H.~McGuire and A.~Pnueli",
 year         = "1993",
 title        = "A Decision Algorithm for Full Propositional Temporal Logic",
 booktitle    = "CAV",
 pages        = "97--109",
 doi          = "10.1007/3-540-56922-7\_9",
)
@inproceedings(MarconiP09,
 author       = "Annapaola Marconi and Marco Pistore",
 year         = "2009",
 title        = "Synthesis and Composition of Web Services",
 booktitle    = "SFM",
 pages        = "89--157",
 doi          = "10.1007/978-3-642-01918-0\_3",
)
@article(MontaliPACMS10,
 author       = "M.~Montali and M.~Pesic and W.~v.d. Aalst and F.~Chesani and P.~Mello",
 year         = "2010",
 title        = "Declarative specification and verification of service choreographies",
 journal      = "TWEB",
 volume       = "4",
 number       = "1",
 doi          = "10.1145/1658373.1658376",
)
@inproceedings(MoskewiczMZZM01,
 author       = "M.~Moskewicz and C.~Madigan and Y.~Zhao and L.~Zhang and S.~Malik",
 year         = "2001",
 title        = "Chaff: Engineering an Efficient SAT Solver",
 booktitle    = "DAC",
 pages        = "530--535",
 url          = "http://www.citeulike.org/user/pwais/article/3403622",
)
@article(Schuppan10,
 author       = "Viktor Schuppan",
 year         = "2010",
 title        = "Towards a notion of unsatisfiable and unrealizable cores for LTL",
 journal      = "Science of Computer Programming",
 doi          = "10.1016/j.scico.2010.11.004",
)
@inproceedings(SheeranSS00,
 author       = "Mary Sheeran and Satnam Singh and Gunnar St{\r a}lmarck",
 year         = "2000",
 title        = "Checking Safety Properties Using Induction and a SAT-Solver",
 booktitle    = "FMCAD",
 pages        = "108--125",
 doi          = "10.1007/3-540-40922-X\_8",
)
@article(Tarjan72,
 author       = "Robert~Endre Tarjan",
 year         = "1972",
 title        = "Depth-First Search and Linear Graph Algorithms",
 journal      = "SIAM J. Comput.",
 volume       = "1",
 number       = "2",
 pages        = "146--160",
 doi          = "10.1137/0201010",
)
@article(XuLW08,
 author       = "K.~Xu and Y.~Liu and C.~Wu",
 year         = "2008",
 title        = "BPSL Modeler - Visual Notation Language for Intuitive Business Property Reasoning",
 journal      = "ENTCS",
 volume       = "211",
 doi          = "10.1016/j.entcs.2008.04.043",
)
@inproceedings(ZhangMMM01,
 author       = "L.~Zhang and C.~Madigan and M.~Moskewicz and S.~Malik",
 year         = "2001",
 title        = "Efficient Conflict Driven Learning in Boolean Satisfiability Solver",
 booktitle    = "ICCAD",
 pages        = "279--285",
 url          = "http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.2715",
)
@inproceedings(ZM03,
 author       = "L.~Zhang and S.~Malik",
 year         = "2003",
 title        = "Extracting small unsatisfiable cores from unsatisfiable Boolean formula.",
 booktitle    = "In Prelim. Proc. Sixth Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT\IeC {\textquoteright }03)",
)