Publications

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

2012

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

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.