Hublet, François; Basin, David; Krstić, Srđan Real-time policy enforcement with metric first-order temporal logic. (English) Zbl 1524.68193 Atluri, Vijayalakshmi (ed.) et al., Computer security – ESORICS 2022. 27th European symposium on research in computer security, Copenhagen, Denmark, September 26–30, 2022. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 13555, 211-232 (2022). MSC: 68Q60 PDFBibTeX XMLCite \textit{F. Hublet} et al., Lect. Notes Comput. Sci. 13555, 211--232 (2022; Zbl 1524.68193) Full Text: DOI
Raszyk, Martin; Basin, David; Traytel, Dmitriy Multi-head monitoring of metric dynamic logic. (English) Zbl 1517.68250 Hung, Dang Van (ed.) et al., Automated technology for verification and analysis. 18th international symposium, ATVA 2020, Hanoi, Vietnam, October 19–23, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12302, 233-250 (2020). MSC: 68Q60 03B44 03B70 PDFBibTeX XMLCite \textit{M. Raszyk} et al., Lect. Notes Comput. Sci. 12302, 233--250 (2020; Zbl 1517.68250) Full Text: DOI
Costa, Gabriele; Galletta, Letterio; Degano, Pierpaolo; Basin, David; Bodei, Chiara Natural projection as partial model checking. (English) Zbl 1468.68124 J. Autom. Reasoning 64, No. 7, 1445-1481 (2020). MSC: 68Q60 68Q45 PDFBibTeX XMLCite \textit{G. Costa} et al., J. Autom. Reasoning 64, No. 7, 1445--1481 (2020; Zbl 1468.68124) Full Text: DOI
Basin, David; Klaedtke, Felix; Zălinescu, Eugen Runtime verification over out-of-order streams. (English) Zbl 1433.68208 ACM Trans. Comput. Log. 21, No. 1, Article No. 5, 43 p. (2020). MSC: 68Q60 03B44 68Q10 68Q85 PDFBibTeX XMLCite \textit{D. Basin} et al., ACM Trans. Comput. Log. 21, No. 1, Article No. 5, 43 p. (2020; Zbl 1433.68208) Full Text: DOI arXiv
Raszyk, Martin; Basin, David; Krstić, Srđan; Traytel, Dmitriy Multi-head monitoring of metric temporal logic. (English) Zbl 1437.68119 Chen, Yu-Fang (ed.) et al., Automated technology for verification and analysis. 17th international symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11781, 151-170 (2019). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{M. Raszyk} et al., Lect. Notes Comput. Sci. 11781, 151--170 (2019; Zbl 1437.68119) Full Text: DOI Link
Schneider, Joshua; Basin, David; Brix, Frederik; Krstić, Srđan; Traytel, Dmitriy Adaptive online first-order monitoring. (English) Zbl 1437.68120 Chen, Yu-Fang (ed.) et al., Automated technology for verification and analysis. 17th international symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11781, 133-150 (2019). MSC: 68Q60 68W27 PDFBibTeX XMLCite \textit{J. Schneider} et al., Lect. Notes Comput. Sci. 11781, 133--150 (2019; Zbl 1437.68120) Full Text: DOI
Basin, David; Bhatt, Bhargav Nagaraja; Krstić, Srđan; Traytel, Dmitriy Almost event-rate independent monitoring. (English) Zbl 1425.68249 Form. Methods Syst. Des. 54, No. 3, 449-478 (2019). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{D. Basin} et al., Form. Methods Syst. Des. 54, No. 3, 449--478 (2019; Zbl 1425.68249) Full Text: DOI Link
Basin, David; Bhatt, Bhargav Nagaraja; Traytel, Dmitriy Optimal proofs for linear temporal logic on lasso words. (English) Zbl 1517.68222 Lahiri, Shuvendu K. (ed.) et al., Automated technology for verification and analysis. 16th international symposium, ATVA 2018, Los Angeles, CA, USA, October 7–10, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11138, 37-55 (2018). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 11138, 37--55 (2018; Zbl 1517.68222) Full Text: DOI
Costa, Gabriele; Basin, David; Bodei, Chiara; Degano, Pierpaolo; Galletta, Letterio From natural projection to partial model checking and back. (English) Zbl 1423.68275 Beyer, Dirk (ed.) et al., Tools and algorithms for the construction and analysis of systems. 24th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 10805, 344-361 (2018). MSC: 68Q60 68Q45 PDFBibTeX XMLCite \textit{G. Costa} et al., Lect. Notes Comput. Sci. 10805, 344--361 (2018; Zbl 1423.68275) Full Text: DOI
Basin, David; Cremers, Cas; Meadows, Catherine Model checking security protocols. (English) Zbl 1392.68228 Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 727-762 (2018). MSC: 68Q60 68M12 94A60 PDFBibTeX XMLCite \textit{D. Basin} et al., in: Handbook of model checking. Cham: Springer. 727--762 (2018; Zbl 1392.68228) Full Text: DOI
Basin, David; Klaedtke, Felix; Zălinescu, Eugen Algorithms for monitoring real-time properties. (English) Zbl 1395.68185 Acta Inf. 55, No. 4, 309-338 (2018). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{D. Basin} et al., Acta Inf. 55, No. 4, 309--338 (2018; Zbl 1395.68185) Full Text: DOI
Torabi Dashti, Mohammad; Basin, David Tests and refutation. (English) Zbl 1495.68141 D’Souza, Deepak (ed.) et al., Automated technology for verification and analysis. 15th international symposium, ATVA 2017, Pune, India, October 3–6, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10482, 119-138 (2017). MSC: 68Q60 PDFBibTeX XMLCite \textit{M. Torabi Dashti} and \textit{D. Basin}, Lect. Notes Comput. Sci. 10482, 119--138 (2017; Zbl 1495.68141) Full Text: DOI
Basin, David; Klaedtke, Felix; Zălinescu, Eugen Runtime verification of temporal properties over out-of-order data streams. (English) Zbl 1494.68160 Majumdar, Rupak (ed.) et al., Computer aided verification. 29th international conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 10426, 356-376 (2017). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 10426, 356--376 (2017; Zbl 1494.68160) Full Text: DOI arXiv
Basin, David; Caronni, Germano; Ereth, Sarah; Harvan, Matúš; Klaedtke, Felix; Mantel, Heiko Scalable offline monitoring of temporal specifications. (English) Zbl 1380.68268 Form. Methods Syst. Des. 49, No. 1-2, 75-108 (2016). MSC: 68Q60 03B70 68M14 PDFBibTeX XMLCite \textit{D. Basin} et al., Form. Methods Syst. Des. 49, No. 1--2, 75--108 (2016; Zbl 1380.68268) Full Text: DOI
Basin, David; Klaedtke, Felix; Zălinescu, Eugen Failure-aware runtime verification of distributed systems. (English) Zbl 1366.68010 Harsha, Prahladh (ed.) et al., 35th IARCS annual conference on foundations of software technology and theoretical computer science, FSTTCS 2015, Bangalore, India, December 16–18, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-97-2). LIPIcs – Leibniz International Proceedings in Informatics 45, 590-603 (2015). MSC: 68M14 03B70 68Q60 68W27 PDFBibTeX XMLCite \textit{D. Basin} et al., LIPIcs -- Leibniz Int. Proc. Inform. 45, 590--603 (2015; Zbl 1366.68010) Full Text: DOI
Basin, David; Klaedtke, Felix; Müller, Samuel; Zălinescu, Eugen Monitoring metric first-order temporal properties. (English) Zbl 1333.68177 J. ACM 62, No. 2, Article No. 15, 45 p. (2015). MSC: 68Q60 03B44 68P15 PDFBibTeX XMLCite \textit{D. Basin} et al., J. ACM 62, No. 2, Article No. 15, 45 p. (2015; Zbl 1333.68177) Full Text: DOI
Basin, David; Klaedtke, Felix; Marinovic, Srdjan; Zălinescu, Eugen Monitoring of temporal first-order properties with aggregations. (English) Zbl 1323.68362 Form. Methods Syst. Des. 46, No. 3, 262-285 (2015). MSC: 68Q60 PDFBibTeX XMLCite \textit{D. Basin} et al., Form. Methods Syst. Des. 46, No. 3, 262--285 (2015; Zbl 1323.68362) Full Text: DOI Link
Basin, David; Keller, Michel; Radomirović, Saša; Sasse, Ralf Alice and Bob meet equational theories. (English) Zbl 1321.68343 Martí-Oliet, Narciso (ed.) et al., Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday. Cham: Springer (ISBN 978-3-319-23164-8/pbk; 978-3-319-23165-5/ebook). Lecture Notes in Computer Science 9200, 160-180 (2015). MSC: 68Q60 68M12 94A60 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 9200, 160--180 (2015; Zbl 1321.68343) Full Text: DOI
Basin, David; Cotrini Jiménez, Carlos; Klaedtke, Felix; Zălinescu, Eugen Deciding safety and liveness in TPTL. (English) Zbl 1371.68101 Inf. Process. Lett. 114, No. 12, 680-688 (2014). MSC: 68Q25 03B44 68Q60 PDFBibTeX XMLCite \textit{D. Basin} et al., Inf. Process. Lett. 114, No. 12, 680--688 (2014; Zbl 1371.68101) Full Text: DOI
Petric Maretić, Grgur; Torabi Dashti, Mohammad; Basin, David LTL is closed under topological closure. (English) Zbl 1296.68097 Inf. Process. Lett. 114, No. 8, 408-413 (2014). MSC: 68Q45 03B44 68Q60 PDFBibTeX XMLCite \textit{G. Petric Maretić} et al., Inf. Process. Lett. 114, No. 8, 408--413 (2014; Zbl 1296.68097) Full Text: DOI
Basin, David; Jugé, Vincent; Klaedtke, Felix; Zălinescu, Eugen Enforceable security policies revisited. (English) Zbl 1354.68165 Degano, Pierpaolo (ed.) et al., Principles of security and trust. First international conference, POST 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28640-7/pbk). Lecture Notes in Computer Science 7215, 309-328 (2012). MSC: 68Q60 68Q85 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 7215, 309--328 (2012; Zbl 1354.68165) Full Text: DOI
Basin, David; Klaedtke, Felix; Müller, Samuel; Pfitzmann, Birgit Runtime monitoring of metric first-order temporal properties. (English) Zbl 1248.68318 Hariharan, Ramesh (ed.) et al., IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2008), December 9–11, 2008, Bangalore, India. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-08-8). LIPIcs – Leibniz International Proceedings in Informatics 2, 49-60, electronic only (2008). MSC: 68Q60 03B44 68P15 PDFBibTeX XMLCite \textit{D. Basin} et al., LIPIcs -- Leibniz Int. Proc. Inform. 2, 49--60 (2008; Zbl 1248.68318) Full Text: DOI Link
Sprenger, Christoph; Basin, David A monad-based modeling and verification toolbox with application to security protocols. (English) Zbl 1144.68306 Schneider, Klaus (ed.) et al., Theorem proving in higher order logics. 20th international conference, TPHOLs 2007, Kaiserslautern, Germany, September 10–13, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74590-7/pbk). Lecture Notes in Computer Science 4732, 302-318 (2007). MSC: 68N18 68Q60 68T15 PDFBibTeX XMLCite \textit{C. Sprenger} and \textit{D. Basin}, Lect. Notes Comput. Sci. 4732, 302--318 (2007; Zbl 1144.68306) Full Text: DOI
Basin, David; Kuruma, Hironobu; Miyazaki, Kunihiko; Takaragi, Kazuo; Wolff, Burkhart Verifying a signature architecture: a comparative case study. (English) Zbl 1111.68075 Formal Asp. Comput. 19, No. 1, 63-91 (2007). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{D. Basin} et al., Formal Asp. Comput. 19, No. 1, 63--91 (2007; Zbl 1111.68075) Full Text: DOI Link
Caleiro, Carlos; Viganò, Luca; Basin, David On the semantics of Alice & Bob specifications of security protocols. (English) Zbl 1153.94450 Theor. Comput. Sci. 367, No. 1-2, 88-122 (2006). MSC: 94A62 68Q55 68Q60 PDFBibTeX XMLCite \textit{C. Caleiro} et al., Theor. Comput. Sci. 367, No. 1--2, 88--122 (2006; Zbl 1153.94450) Full Text: DOI
Basin, David; Kuruma, Hironobu; Takaragi, Kazuo; Wolff, Burkhart Verification of a signature architecture with HOL-Z. (English) Zbl 1120.68407 Fitzgerald, John (ed.) et al., FM 2005: Formal methods. International symposium of formal methods Europe, Newcastle, UK, July 18–22, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27882-6/pbk). Lecture Notes in Computer Science 3582, 269-285 (2005). MSC: 68Q60 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 3582, 269--285 (2005; Zbl 1120.68407) Full Text: DOI
Basin, David; Deville, Yves; Flener, Pierre; Hamfelt, Andreas; Fischer Nilsson, Jørgen Synthesis of programs in computational logic. (English) Zbl 1080.68562 Bruynooghe, Maurice (ed.) et al., Program development in computational logic. A decade of research advances in logic-based program development. Berlin: Springer (ISBN 3-540-22152-2/pbk). Lecture Notes in Computer Science 3049, 30-65 (2004). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 3049, 30--65 (2004; Zbl 1080.68562) Full Text: DOI
Basin, David; Friedrich, Stefan; Gawkowski, Marek Bytecode verification by model checking. (English) Zbl 1031.68038 J. Autom. Reasoning 30, No. 3-4, 399-444 (2003). MSC: 68N15 68N30 PDFBibTeX XMLCite \textit{D. Basin} et al., J. Autom. Reasoning 30, No. 3--4, 399--444 (2003; Zbl 1031.68038) Full Text: DOI
Basin, David; Friedrich, Stefan; Gawkowski, Marek; Posegga, Joachim Bytecode model checking: An experimental analysis. (English) Zbl 1077.68678 Bošnački, Dragan (ed.) et al., Model checking software. 9th international SPIN workshop, Grenoble, France, April 11–13, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43477-1). Lect. Notes Comput. Sci. 2318, 42-59 (2002). MSC: 68Q60 68N19 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 2318, 42--59 (2002; Zbl 1077.68678) Full Text: Link
Basin, David; Friedrich, Stefan; Gawkowski, Marek Verified bytecode model checkers. (English) Zbl 1013.68544 Carreño, Victor A. (ed.) et al., Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2410, 47-66 (2002). MSC: 68T15 03B35 68Q60 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 2410, 47--66 (2002; Zbl 1013.68544) Full Text: Link
Armando, Alessandro; Basin, David; Bouallagui, Mehdi; Chevalier, Yannick; Compagna, Luca; Mödersheim, Sebastian; Rusinowitch, Michael; Turuani, Mathieu; Viganò, Luca; Vigneron, Laurent The AVISS security protocol analysis tool. (English) Zbl 1010.68795 Brinksma, Ed (ed.) et al., Computer aided verification. 14th international conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2404, 349-353 (2002). MSC: 68U99 68Q60 68P25 PDFBibTeX XMLCite \textit{A. Armando} et al., Lect. Notes Comput. Sci. 2404, 349--353 (2002; Zbl 1010.68795) Full Text: Link
Basin, David; Clavel, Manuel; Meseguer, José Rewriting logic as a metalogical framework. (English) Zbl 1044.03020 Kapoor, Sanjiv (ed.) et al., FST TCS 2000: Foundations of software technology and theoretical computer science. 20th conference, New Delhi, India, December 13–15, 2000. Proceedings. Berlin: Springer (ISBN 3-540-41413-4). Lect. Notes Comput. Sci. 1974, 55-80 (2000). MSC: 03B70 68Q42 68T15 68Q60 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 1974, 55--80 (2000; Zbl 1044.03020) Full Text: Link
Ayari, Abdelwaheb; Basin, David Bounded model construction for monadic second-order logics. (English) Zbl 0974.68115 Emerson, E. Allen (ed.) et al., Computer aided verification. 12th international conference, CAV 2000. Chicago, IL, USA, July 15-19, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1855, 99-112 (2000). MSC: 68Q60 03B15 03B25 68Q45 PDFBibTeX XMLCite \textit{A. Ayari} and \textit{D. Basin}, Lect. Notes Comput. Sci. 1855, 99--112 (2000; Zbl 0974.68115)
Basin, David; Denker, Grit Maude versus Haskell: An experimental comparison in security protocol analysis. (English) Zbl 0962.68056 Futatsugi, Kokichi, The 3rd international workshop on rewriting logic and its applications, RWLW. Kanazawa City Cultural Hall, Kanzawa, Japan, September 18-20, 2000. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 36, 22 p., electronic only (2000). MSC: 68P25 68Q60 68Q42 68N15 PDFBibTeX XMLCite \textit{D. Basin} and \textit{G. Denker}, in: The 3rd international workshop on rewriting logic and its applications, RWLW. Kanazawa City Cultural Hall, Kanzawa, Japan, September 18--20, 2000. Amsterdam: Elsevier. 22 p. (2000; Zbl 0962.68056)
Basin, David; Friedrich, Stefan; Posegga, Joachim; Vogt, Harald Java bytecode verification by model checking. System abstract. (English) Zbl 1046.68575 Halbwachs, Nicolas (ed.) et al., Computer aided verification. 11th international conference, CAV ’99. Trento, Italy, July 6–10, 1999. Proceedings. Berlin: Springer (ISBN 3-540-66202-2). Lect. Notes Comput. Sci. 1633, 491-494 (1999). MSC: 68Q60 68N15 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 1633, 491--494 (1999; Zbl 1046.68575)
Ayari, Abdelwaheb; Basin, David; Podelski, Andreas LISA: A specification language based on WS2S. (English) Zbl 0908.03036 Nielsen, Mogens (ed.) et al., Computer science logic. 11th international workshop, CSL ’97. Annual conference of the EACSL, Aarhus, Denmark, August 23–29, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1414, 18-34 (1998). MSC: 03B70 68Q60 03D05 03B25 PDFBibTeX XMLCite \textit{A. Ayari} et al., Lect. Notes Comput. Sci. 1414, 18--34 (1998; Zbl 0908.03036)
Basin, David; Matthews, Seán A conservative extension of first-order logic and its applications to theorem proving. (English) Zbl 0924.03103 Shyamasundar, R. K. (ed.), Foundations of software technology and theoretical computer science. 13th conference, Bombay, India, December 15-17, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 761, 151-160 (1993). MSC: 03F05 03B20 03B35 03B70 68Q60 PDFBibTeX XMLCite \textit{D. Basin} and \textit{S. Matthews}, Lect. Notes Comput. Sci. 761, 151--160 (1993; Zbl 0924.03103)
Basin, David A.; Constable, Robert L. Metalogical frameworks. (English) Zbl 0922.03019 Huet, Gérard (ed.), Logical environments. Cambridge: Univ. Press. 1-29 (1993). MSC: 03B35 68T15 03B70 68N01 68Q60 PDFBibTeX XMLCite \textit{D. A. Basin} and \textit{R. L. Constable}, in: Logical environments. Cambridge: Univ. Press. 1--29 (1993; Zbl 0922.03019)