Publications

Please click on the paper’s title to request a paper.

2014

Monitoring with Data Automata. K. Havelund ISoLA 2014 In Kim Larsen and Axel Legay, editors, 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. Track: Statistical Model Checking, Past Present and Future. 8-11 October 2014 - Imperial, Corfu, Greece. LNCS, Springer-Verlag.

Data Automata in Scala. K. Havelund TASE 2014, In Martin Leucker and Ji Wang, editors, The 8th International Symposium on Theoretical Aspects of Software Engineering. 1-3 September 2014 - Changsha, China. IEEE Computer Society Press. Invited presentation.

Tools and Algorithms for the Construction and Analysis of Systems Ed. Erika Ábrahám and Klaus Havelund - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings

Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations. Khalil Ghorbal and Andrew Sogokon and André Platzer in Static Analysis, ed. Markus Müller-Olm and Helmut Seidl- 21th International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Springer

Characterizing Algebraic Invariants by Differential Radical Invariants. Khalil Ghorbal and André Platzer. TACAS 2014, pages 279-294, 2014.

A Galois connection calculus for abstract interpretation. Patrick Cousot, Radhia Cousot: POPL 2014: 3-4

Collaborative verification-driven engineering of hybrid systems. Stefan Mitsch, Grant Olney Passmore and André Platzer. Mathematics in Computer Science, 8(1), pages 71-97, 2014.

Refactoring, refinement, and reasoning: A logical characterization for hybrid systems. Stefan Mitsch, Jan-David Quesel and André Platzer. In Cliff B. Jones, Pekka Pihlajasaari and Jun Sun, editors, 19th International Symposium on Formal Methods, FM, Singapore, Proceedings, volume 8442 of LNCS, pages 481-496. Springer, 2014.

A Menagerie of Timed Automata. Peter Fontana and Rance Cleaveland. To Appear in the Journal of Computing Surveys, September 2014, 58 pages. doi: 10.1145/2518102

2013

A Scala DSL for Rete-based Runtime Verification K. Havelund The 4th International Conference on Runtime Verification (RV 2013) Rennes, France, September 24-27, 2013. Lecture Notes in Computer Science, Vol. 8174.

Verification & Validation Meets Planning & Scheduling S. Bensalem, K. Havelund, and A. Orlandini International Journal on Software Tools for Technology Transfer (STTT) 16(1) 2014. Introduction article to special issue containing selected submissions for the 3rd ICAPS workshop on Verification & Validation of Planning & Scheduling Systems (VVPS 2011). Also presented at MOCHAP 2014, Workshop on Model Checking and Automated Planning, Portsmouth, NH, USA, June 21-26, 2014. Affiliated with ICAPS 2014, the 24th International Conference on Automated Planning and Scheduling.

Rule-based Runtime Verification Revisited K. Havelund International Journal on Software Tools for Technology Transfer (STTT). Special issue containing selected submissions for the 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2012) Track: Runtime Verication, the Application Perspective. April 2013.

Formal Verification of Behavioral Models of Phase-Locked Loops (PLLs) Made Tractable With New Methods for Computing Reachable Sets for Hybrid Dynamic Systems M. Althoff, A. Rajhans, B. H. Krogh, S. Yaldiz, X. Li, L. Pileggi, Communications of the ACM, Vol. 56 No. 10, Pages 97-104, 2013 (Originally published in ICCAD '11, Best Paper Award)

Cancer Hybrid Automata: Model, Beliefs & Therapy. Loes Olde Loohuis, Andreas Witzel, Bud Mishra (2013). Special Issue of Information and Computation on "Hybrid Systems and Biology". (Accepted).

Power-law Null Model for Bystander Mutations in Cancer. Loes Olde Loohuis, Andreas Witzel, Bud Mishra (2013). IEEE Trans on Comp. Biology and Bioinformatics. (under review).

What can information-asymmetric games tell us about the context of Crick’s “Frozen Accident”?. Justin Jee, Andrew Sundstrom, Steven Massey, Bud Mishra (2013). Journal of the Royal Society Interface.

Formal verification of distributed aircraft controllers. Sarah M. Loos, David W. Renshaw, and André Platzer, In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pages 125-130. ACM, 2013.

Certifying the safe design of a virtual fixture control algorithm for a surgical robot. Yanni Kouskoulas, David W. Renshaw, André Platzer and Peter Kazanzides. In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pages 263-272. ACM, 2013.

Bayesian statistical model checking with application to Simulink/Stateflow verification. Paolo Zuliani, André Platzer, and Edmund M. Clarke, Formal Methods in System Design, pages 1-30, 2013.

Teaching CPS foundations with contracts. André Platzer, First Workshop on Cyber-Physical Systems Education, pages 7-10. 2013.

Structural Counter Abstraction. K. Bansal, E. Koskinen, T. Wies, D. Zufferey. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013). June 2013.

Landing a Spacecraft on Mars. G.J. Holzmann, IEEE Software, Impact Column, March/April 2013, pp. 17-20.

A Three-Step Program for Recovering Hackers. G.J. Holzmann, IEEE Computer, June 2013, pp. 10-12.

Proving Properties of Concurrent Programs. G.J. Holzmann, Proc. 20th Spin Workshop (First Spin Symposium), July 2013, LNCS 7976, Springer-Verlag, pp. 18-23.

Reasoning about Nondeterminism in Programs. B Cook, E Koskinen. To appear in Proceedings of the ACM SIGPLAN 2013 Conference on Programming Language Design and Implementation (PLDI 2013). June 2013.

Curvature Analysis of Cardiac Excitation Wavefronts. Abhishek Murthy, Ezio Bartocci, Flavio H. Fenton, James Glimm, Richard A. Gray, Elizabeth Cherry, Scott A. Smolka, Radu Grosu, IEEE/ACM Transactions on Computational Biology and Bioinformatics 10(2): 323-336 (2013).

Compositionality Results for Cardiac Cell Dynamics. Md. Ariful Islam, Abhishek Murthy, Ezio Bartocci, Antoine Girard, Scott A. Smolka and Radu Grosu. In Proceedings of CMSB'13, the 11th Conference on Computational Methods in Systems Biology, Klosterneuburg, Austria, September, 2013. Springer LNCS. (Short paper)

2012

Theories, solvers and static analysis by abstract interpretation. Patrick Cousot, Radhia Cousot, Laurent Mauborgne (2012). Journal of the ACM. 59 (6).

The structure of differential invariants and differential cut elimination. André Platzer, Logical Methods in Computer Science, 8(4), pages 1-38, 2012.

Statistical model checking for Markov decision processes. David Henriques, João G. Martins, Paolo Zuliani, André Platzer, and Edmund M. Clarke, In 9th International Conference on Quantitative Evaluation of Systems, QEST 2012, September 17-20, London, UK, pages 84-93. IEEE Computer Society, 2012.

A differential operator approach to equational differential invariants. André Platzer , In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, International Conference, ITP 2012, August 13-15, Princeton, USA, Proceedings, volume 7406 of LNCS, pages 28-48. Springer, 2012.

Logics of dynamical systems. André Platzer, ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012.

A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. André Platzer, Logical Methods in Computer Science, 8(4), pages 1-44, 2012. Special issue for selected papers from CSL'10.

Approximate Bisimulations for Sodium Channel Dynamics, Abhishek Murthy, Md. Ariful Islam, Ezio Bartocci, Elizabeth Cherry, Flavio H. Fenton, James Glimm, Scott A. Smolka, Radu Grosu: . CMSB 2012: 267-287

Parallelizing the Spin Model Checker. G.J. Holzmann, Proc. 19th Int. Spin Workshop, Oxford, England, 23-24 July 2012, Springer, LNCS 7385, pp. 155-171.

Logic model checking of time-periodic real-time systems. M. Florian, E. Gamble, G.J. Holzmann, Proc. Infotech@Aerospace Conference, AIAA, Garden Grove, CA, June 2012 (invited).

Quantified Event Automata - Towards Expressive and Efficient Runtime Monitors. Howard Barringer, Ylies Falcone, Klaus Havelund, Giles Reger, and David Rydeheard, 18th International Symposium on Formal Methods, Paris, France. August 27-31, 2012. Lecture Notes in Computer Science.

A Tutorial on Runtime Verification. Ylies Falcone, Klaus Havelund, and Giles Reger. Book chapter in: Summer School Marktoberdorf 2012 - Engineering Dependable Software Systems. IOS Press, in print.

Closing the Gap Between Specification and Programming: VDM++ and Scala. Klaus Havelund HOWARD-60 - Higher-Order Workshop on Automated Runtime Verification and Debugging. December 20, 2011, Manchester, UK. EasyChair Proceedings Volume 1 (first edition).

What does AI have to do with RV? - Extended Abstract. Klaus Havelund. ISoLA'12 special track on Runtime Verification: the application perspective. October 15-18, 2012, Heraklion, Crete. Lecture Notes in Computer Science.

Focus on Personalized Molecular based Medicine. LHT. Van der Ploeg, B. Mishra, C. Eitner, J. Burrows, T. Tombler, V. Poponin, D. Knauer, I. Ichetovkin, R. Pinnola, G. Endress, P. Soon-Shiong. Biomarkers in Oncology: Predictions and Prognosis, (edited by Heinz-Josef Lenz, MD), Springer-Verlag, NY, January 2012.

Towards Cancer Hybrid Automata. Loes Olde Loohuis, Andreas Witzel, Bud Mishra. First International Workshop on Hybrid Systems and Biology: HSB 2012, Newcasle upon Tyne, UK, September 3, 2012.

Reverse Engineering Dynamic Temporal Models of Biological Processes and their Relationships.Marco Antoniotti, N. Ramakrishnan, Bud Mishra. Proc. National Academy of Science U S A, 107(28):12511-6, 2010.

Probabilistic Abstract Interpretation. Patrick Cousot, Michael Monerau:. Helmut Seidl (Ed.): Programming Languages and Systems - 21st European Symposium on Programming, ESOP 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. Lecture Notes in Computer Science 7211 Springer 2012: 169-193.

Formal Verification by Abstract Interpretation. Patrick Cousot, Alwyn Goodloe, Suzette Person (Eds.): NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. Lecture Notes in Computer Science 7226 Springer 2012: 3-7.

A semantic integrated development environment. Francesco Logozzo, Michael Barnett, Manuel Fähndrich, Patrick Cousot, Radhia Cousot: Gary T. Leavens (Ed.): Conference on Systems, Programming, and Applications: Software for Humanity, SPLASH '12, Tucson, AZ, USA, October 21-25, 2012: 15-16.

An abstract interpretation framework for refactoring with application to extract methods with contracts. Patrick Cousot, Radhia Cousot, Francesco Logozzo, Michael Barnett: Gary T. Leavens, Matthew B. Dwyer (Eds.): Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012. ACM 2012: 213-232.

An abstract interpretation framework for termination. Patrick Cousot, Radhia Cousot: John Field, Michael Hicks (Eds.): Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012. ACM 2012: 245-258.

Automatic inference of necessary preconditions. Patrick Cousot, Radhia Cousot, Manuel Fähndrich, Francesco Logozzo: Roberto Giacobazzi, Isabella Mastroeni (Eds.): Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2011, Roma, Italy, January 20-22, 2013. Proceedings. Lecture Notes in Computer Science, Springer 2013. (To appear)

A New Stochastic Derivative Estimator for Discontinuous Payoff Functions with Application to Financial Derivatives. Y. Wang, M.C. Fu, S.I. Marcus. In Operations Research. (To appear)

INTERASPECT: Aspect-Oriented Instrumentation with GCC. J. Seyster, K. Dixit, X. Huang, R. Grosu, K. Havelund, S.A. Smolka, S.D. Stoller, E. Zadok. In Formal Methods in System Design. (To appear)

Coordinate ascent for penalized semiparametric regression on high-dimensional panel count data. T.T. Wu and X. He. In Computational Statistics and Data Analysis, Volume 56, Issue 1, 1 January 2012, Pages 25 - 33.

A transcriptome analysis by lasso penalized Cox regression for pancreatic cancer survival. T.T. Wu, H. Gong, and E.M. Clarke. In Journal of Bioinformatics and Computational Biology. To appear.

2011

Model checking multitask applications for OSEK compliant real-time operating systems. M. McKelvin, and G.J. Holzmann, Proc. 17th IEEE Pacific Rim Int. Symposium on Dependable Computing (PRDC 2011) Pasadena, CA, Dec. 12-14, 2011.

Quantified Differential Invariants. A. Platzer. In HSCC 2011: Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, pp 63-72, 2011.

Software Certification – Coding, Code, and Coders. K. Havelund, G.J. Holzmann. In EMSOFT ’11: Proceedings of the 11th International Conference on Embedded Software, pp 205-210, 2011.

Internal versus External DSLs for Trace Analysis. (Extended abstract for tutorial.) H. Barringer, K. Havelund. In RV ’11: Proceedings of the 2nd International Conference on Runtime Verification, Springer LNCS. (To appear)

Linear Absolute Value Relation Analysis. L. Chen, A. Miné, J. Wang, P. Cousot. In ESOP 2011: Proceedings of the 20th European Symposium on Programming, LNCS 6602, pp. 156-175, 2011.

The Reduced Product of Abstract Domains and the Combination of Decision Procedures. P. Cousot, R. Cousot, L. Mauborgne. In FOSSACS 2011: 14th International Conference on the Foundations of Software Science and Computational Structures, LNCS 6604, pp. 456-472, 2011.

A parametric segmentation functor for fully automatic and scalable array content analysis. P. Cousot, R. Cousot, F. Logozzo. In POPL 2011: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 105-118, 2011.

Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. P. Cousot, R. Cousot, F. Logozzo. In VMCAI 2011: 12th International Conference on Verification, Model Checking, and Abstract Interpretation, LNCS 6538, pp. 150-168, 2011.

Runtime Verification with State Estimation. S.D. Stoller, E. Bartocci, J. Seyster, R. Grosu, K. Havelund, S.A. Smolka, and E. Zadok. In RV'11: Proceedings of the 2nd International Conference on Runtime Verification, Springer LNCS. To appear. (Best Paper Award)

Teaching cardiac electrophysiology modeling to undergraduate students: laboratory exercises and GPU programming for the study of arrhythmias and spiral wave dynamics. E. Bartocci, R. Singh, F. von Stein, A. Amedome, Alan-Joseph Caceres, J. Castillo, E. Closser, G. Deards, A. Goltsev, R. Sta. Ines, C. Isbilir, J. Marc, D. Moore, D. Pardi, S. Sadhu, S. Sanchez, P. Sharma, A. Singh, J. Rogers, A. Wolinetz, T. Grosso-Applewhite, K. Zhao, A. Filipski, R. Gilmour Jr, R. Grosu, J. Glimm, S. A. Smolka, E. Cherry, E. Clarke, N. Griffeth, and F. Fenton. Journal of Advances in Physiology of Education. To appear.

Curvature Analysis of Cardiac Dynamics. A. Murthy, E. Bartocci, F. Fenton, J. Glimm, S. A. Smolka and R. Grosu. In CMSB 2011: Proceedings of the 9th ACM International Conference on Computational Methods in Systems Biology, pages 151-160. ACM, 2011.

Toward Real-Time Simulation of Cardiac Dynamics. E. Bartocci, E. M. Cherry, J. Glimm, R. Grosu, S. A. Smolka and F. Fenton. In CMSB 2011: Proceedings of the 9th ACM International Conference on Computational Methods in Systems Biology, pages 103-110. ACM, 2011.

Formal Verification of Phase-Locked Loops Using Reachability Analysis and Continuization. M. Althoff, A. Rajhans, B. H. Krogh, S. Yaldiz, X. Li, L. Pileggi. In ICCAD 2011: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design. To appear. (Best Paper Award)

Zonotope Bundles for the Efficient Computation of Reachable Sets. M. Althoff and B. H. Krogh. In CDC-ECC 2011: Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference. To appear.

Set-Based Computation of Vehicle Behaviors for the Online Verification of Autonomous Vehicles. M. Althoff and J. M. Dolan. In ITSC’11: Proceedings of the 14th International IEEE Conference on Intelligent Transportation Systems, 2011.

Quantifier Elimination over Finite Fields Using Grobner Bases. S. Gao, A. Platzer, and E.M. Clarke. In CAI 2011: Proceedings of the 4th International Conference on Algebraic Informatics, LNCS 6742, pp. 140-157, 2011.

Using Continuization in Reachability Analysis for the Verification of a Phase-Locked Loop. M. Althoff, A. Rajhans, B. H. Krogh, S. Yaldiz, X. Li, L. Pileggi. In Proceedings of Frontiers in Analog Circuit (FAC) Synthesis and Verification, Snowbird, Utah, July 2011.

From Cardiac Cells to Genetic Regulatory Networks. R. Grosu, G. Batt, F. H. Fenton, J. Glimm, C. Le Guernic, S. A. Smolka, E. Bartocci. In CAV 2011: Proceedings of the 23rd International Conference on Computer-Aided Verification, LNCS 6806, pp. 396-411, 2011.

SpaceEx: Scalable verification of hybrid systems. G. Frehse, C. Le Guernic, A. Donzé, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. In CAV 2011: Proceedings of the 23rd International Conference on Computer-Aided Verification, LNCS 6806, pp. 379-395, 2011.

Statistical model checking for distributed probabilistic control hybrid automata with smart grid applications. J. G. Martins, A. Platzer, and J. Leite. In ICFEM 2011: Proceedings of the International Conference on Formal Engineering Methods, LNCS 6991, 2011.

Distributed theorem proving for distributed hybrid systems. D. W. Renshaw, S. M. Loos, and A. Platzer. In ICFEM 2011: Proceedings of the International Conference on Formal Engineering Methods, LNCS 6991, 2011.

Safe intersections: At the crossing of hybrid systems and verification. S. M. Loos and A. Platzer. In ITSC’11: Proceedings of the 14th International IEEE Conference on Intelligent Transportation Systems, 2011.

Logic and compositional verification of hybrid systems. A. Platzer. In CAV 2011: Proceedings of the 23rd International Conference on Computer-Aided Verification, LNCS 6806, pp 28-43. (Invited tutorial)

Using Integer Clocks to Verify Clock-Synchronization Protocols. X. Huang, A. Singh, and S. A. Smolka. Innovations in Systems and Software Engineering, Special Issue on NASA Formal Methods Symposium 2010, Vol. 7, Issue 2, pp. 119-130 (June 2011).

On the Energy Consumption and Performance of Systems Software. Z. Li, R. Grosu, P. Sehgal, S. A. Smolka, E. Zadok. Proceedings of SYSTOR '11, Fourth Annual International Conference on Systems and Storage, ACM Press, pp: 8:12, 2011.

Regulatory Network Analysis Acceleration with Reconfigurable Hardware. N. Miskov-Zivanov, A. Bresticker, S. Venkatakrishnan, P. Kashinkunti, D.  Krishnaswamy, D. Marculescu and J. R. Faeder. Proceedings of the International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC), September 2011, to appear.

Emulation of Biological Networks in Reconfigurable Hardware. N. Miskov-Zivanov, A. Bresticker, D. Krishnaswamy, S. Venkatakrishnan, D. Marculescu and J. R. Faeder. Proceedings of the ACM Conference on Bioinformatics, Computational Biology and Biomedicine (ACM-BCB), August 2011, to appear.

Model Checking of a Diabetes-Cancer Model. H. Gong, P. Zuliani, E. M. Clarke. In CMLS 2011: 3rd International Symposium on Computational Models for Life Sciences, AIP Conf. Proc. 1371, pages 234-243, 2011.

Model Repair for Probabilistic Systems. E. Bartocci, R. Grosu, P. Katsaros, C.R. Ramakrishnan, S. A. Smolka. In TACAS 2011: Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 6605, pp. 326–340, 2011.

Analog Circuit Verification by Statistical Model Checking. Y.-C. Wang, A. Komuravelli, P. Zuliani, E. M. Clarke. In ASP-DAC 2011: Proceedings of the 16th Asia and South Pacific Design Automation Conference, January 25-28, 2011, Tokyo, Japan. (Best Paper Award nomination).

Symbolic Model Checking of Signaling Pathways in Pancreatic Cancer. H. Gong, Q. Wang, P. Zuliani, J. R. Faeder, M. T. Lotze, E. M. Clarke. In BiCoB 2011: 3rd International Conference on Bioinformatics and Computational Biology, March 23-25, 2011, New Orleans, LA.

Reachable Set Computation for Uncertain Time-Varying Linear Systems. M. Althoff and C. Le Guernic and B. H. Krogh. In HSCC 2011: Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, April 12-14, Chicago, USA.

Analyzing Reachability of Linear Dynamic Systems with Parametric Uncertainties. (Book Chapter) M. Althoff and B. H. Krogh and O. Stursberg. In Modeling, Design, and Simulation of Systems with Uncertainties. A. Rauh and E. Auer, editors. Springer, 2011.

View Consistency in Architectures for Cyber-Physical Systems. A. Bhave, B. Krogh,  D. Garlan, and B. Schmerl. In Proceedings of the 2nd ACM/IEEE International Conference on Cyber-Physical Systems, April 12-14, 2011.

 

2010

Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification. P. Zuliani, A. Platzer, E.M. Clarke. In HSCC ’10: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp 243-252, 2010.

Model-based Evolutionary Optimization. Y. Wang, M.C. Fu, S.I. Marcus. In WSC ’10: Proceedings of the 2010 Winter Simulation Conference, pp 1199-1210, 2010.

Logical Abstract Domains and Interpretations. P. Cousot, R. Cousot, L. Mauborgne. In FSE 2010: The Future of Software Engineering, Springer, pp. 48-71.

A Scalable Segmented Decision Tree Abstract Domain. P. Cousot, R. Cousot, L. Mauborgne. Essays in Memory of Amir Pnueli, LNCS 6200, pp. 72-95, 2010.

Analysis and Verification of the HMGB1 Signaling Pathway. H. Gong, P. Zuliani, A. Komuravelli, J. R. Faeder, E. M. Clarke. BMC Bioinformatics 2010, 11(Suppl 7):S10. (Best Paper Award at InCoB 2010)

Computational Modeling and Verification of Signaling Pathways in Cancer. H. Gong, P. Zuliani, A. Komuravelli, J. R. Faeder, E. M. Clarke. In ANB 2010: Proceedings of Algebraic and Numeric Biology. LNCS  volume 6479, Springer, 2010.

Statistical Verification of Probabilistic Properties with Unbounded Until. H. L. S. Younes, E. M. Clarke, P. Zuliani. In SBMF 2010: Proceedings of the 13th Brazilian Symposium on Formal Methods. LNCS volume 6527, pages 144-160, Springer, 2011.

Augmenting Software Architectures with Physical Components. A. Bhave, D. Garlan, B. Krogh, A. Rajhans, and B. Schmerl. In Proceedings of Embedded Real-Time Software and Systems (ERTS), May 2010, Toulouse, France.

Multicategory Vertex Discriminant Analysis for High-Dimensional Data. T.T. Wu and K. Lange. Annals of Applied Statistics, Volume 4, No 4, 1698-1721, 2010.

Semiparametric Additive Risks Regression for Two-Stage Design Survival Studies. G. Li  and T.T. Wu. Statistica Sinica, Volume 20, No 4, 1581-1607, 2010.

Quantified differential dynamic logic for distributed hybrid systems. A. Platzer. In CSL ’10: Proceedings of Computer Science Logic, 19th EACSL Annual Conference, Brno, Czech Republic, August 23-27, 2010. Volume 6247 of LNCS, pages 469-483. Springer, 2010.

Automated Assume-Guarantee Reasoning through Implicit Learning. Y.-F. Chen, E. M. Clarke, A. Farzan, M.-H. Tsai, Y.-K. Tsay, B.-Y. Wang. In CAV ‘10: 22nd International Conference on Computer Aided Verification. LNCS volume 6174, pages 511-526, Springer 2010.

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. Y.-F. Chen, E. M. Clarke, A. Farzan, F. He, M.-H. Tsai, Y.-K. Tsay, B.-Y. Wang, L. Zhu. In ISolA ’10: 4th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation. LNCS volume 6415, pages 643-657, Springer 2010.

A Non-prenex, Non-clausal QBF Solver with Game-State Learning. W. Klieber, S. Sapra, S. Gao, E. M. Clarke. In SAT ’10: 13th International Conference on Theory and Applications of Satisfiability Testing. LNCS volume 6175, pages 128-142, Springer 2010.

Aspect-Oriented Instrumentation with GCC. J. Seyster, K. Dixit, X. Huang, R. Grosu, K. Havelund,S. A. Smolka, S. D. Stoller and E. Zadok. Proceedings of RV 2010, First International Conference on Runtime Verification, LNCS 6418, pp. 405-420, 2010.

Formal Analysis of the Kaminsky DNS Cache-Poisoning Attack Using Probabilistic Model Checking. N. Alexiou, T. Deshpande, S. Basagiannis, S. A. Smolka and P. Katsaros. Proceedings of HASE 2010, 12th IEEE International High Assurance Systems Engineering Symposium, San Jose, CA, IEEE Computer Society (Nov. 2010).

On Incrementally Bounded Systems. J. Kapinski and B. H. Krogh. In Proceedings of the 2010 American Control Conference.

On zone-based analysis of duration probabilistic automata. O. Maler, K. Larsen, B.H. Krogh. In Proceedings of the 12th International Workshop on Verification of Infinite-State Systems (INFINITY 2010).

On a novel coalescent model for genome-wide evolution of Copy Number Variations. A. Mitrofanova and B. Mishra. In International Journal of Data Mining and Bioinformatics 2010 - Vol. 4, No.3, pp. 300 – 315.

 

2009

European Train Control System: A case study in formal verification. A. Platzer and J.-D. Quesel. In ICFEM ‘09, 11th International Conference on Formal Engineering Methods, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pages 246-265. Springer, 2009.