@conference {,
	title = {Model-Checking Support for File System Development},
	booktitle = {Proceeding of HotStorage {\textquoteright}21, the 13th ACM Workshop on Hot Topics in Storage and File Systems},
	year = {2021},
	month = {07/2021},
	author = {W. Su and Y. Liu and G. Ganesan and G. Holzmann and G. Kuenning and S. A. Smolka and E. Zadok}
}
@article {,
	title = {Accelerating simulations of cardiac electrical dynamics through a multi-GPU platform and an optimized data structure},
	journal = {Concurrency and Computation: Practice and Experience},
	volume = {32},
	year = {2020},
	month = {03/2020},
	url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&cstart=20\&pagesize=80\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:vDijr-p_gm4C},
	author = {Eduardo C Vasconcellos and Esteban WG Clua and Flavio H Fenton and Marcelo Zamith}
}
@article {,
	title = {Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems},
	journal = {IEEE Access},
	year = {2020},
	author = {F. Shmarov and S. Soudjani and N. Paoletti and E. Bartocci and S. Lin and S. A. Smolka and P. Zuliani}
}
@conference {,
	title = {Neural State Classification for Hybrid Systems},
	booktitle = {Proc.\ 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018)},
	year = {2018},
	publisher = {Springer-Verlag},
	organization = {Springer-Verlag},
	author = {Dung Phan and Nicola Paoletti and Timothy Zhang and Radu Grosu and Scott A. Smolka and Scott D. Stoller}
}
@conference {,
	title = {{SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems}},
	booktitle = {Haifa Verification Conference, to appear},
	year = {2017},
	abstract = {<p>Abstract. We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particular, we consider hybrid systems with nonlinear dynamics (Lipschitzcontinuous ordinary differential equations) and random parameters, and we synthesize PID controllers such that the resulting closed-loop systems satisfy safety and performance constraints given as probabilistic bounded reachability properties. Our technique leverages SMT solvers over the reals and nonlinear differential equations to provide formal guarantees that the synthesized controllers satisfy such properties. These controllers are also robust by design since they minimize the probability of reaching an unsafe state in the presence of random disturbances. We apply our approach to the problem of insulin regulation for type 1 diabetes, synthesizing controllers with robust responses to large random meal disturbances, thereby enabling them to maintain blood glucose levels within healthy, safe ranges.</p>
},
	author = {Fedor Shmarov and Nicola Paoletti and Ezio Bartocci and Shan Lin and Scott Smolka and Paolo Zuliani}
}
