Tuesday, January 19, 2021

[DMANET] Two open Ph.D. positions in Probabilistic Verification Methodologies

Two Open PhD positions in Probabilistic Verification Methodologies for
Synthetic Biology and Nanotechnology at Utah State University

Both Ph.D. positions are available at Utah State University in the U.S.
They are fully funded Ph.D. positions for three years with the possibility
of one-year extension. The expected starting date is late August, 2021. GRE
requirement is temporarily suspended until further notice. Graduate
application deadline closes on May 1st, 2021.

Abstract:
Synthetic biology and nanotechnology place increasing demands on design
methodologies to ensure dependable and robust operation. Consisting of
noisy and unreliable components, these complex systems have large and often
infinite state spaces that include extremely rare error states.
Probabilistic model checking techniques have demonstrated significant
potential in quantitatively analyzing such system models under extremely
low probability. Unfortunately, they generally require enumerating the
model's state space, which is computationally intractable or impossible.
Therefore, addressing these design challenges in emerging technologies
requires enhancing the applicability of probabilistic model checking.
Motivated by this problem, this project investigates an automated
probabilistic verification framework that integrates approximate
probabilistic model checking and counterexample-guided rare-event
simulation to improve the analysis accuracy and efficiency. This
multi-institution collaborative project focuses on verifying infinite-state
continuous-time Markov chain (CTMC) models with rare-event properties. It
addresses the scalability problem by first applying property-guided and
on-the-fly state truncation techniques to prune unlikely states to obtain
finite state representations that are amenable to probabilistic model
checking. In the case of false or indeterminate verification results,
probabilistic counterexamples are generated and utilized to improve the
accuracy of the state reductions. Furthermore, it mines these critical
counterexamples as automated guidance to improve the quality and efficiency
for rare-event probabilistic simulations. This verification framework will
be integrated within existing state-of-the-art probabilistic model checking
tools (e.g., the PRISM model checking tool), and benchmarked on a wide
range of real-world case studies in synthetic biology and nanotechnology.
========================================

Project description:
The first position will be advancing and developing efficient state space
truncation and model abstraction techniques for the infinite-state CTMC
models. In particular, we are interested in investigating:
- Algorithms for state space truncation for infinite-state probabilistic
systems with improved accuracy;
- Prototype implementation of the developed algorithms in Java;
- Evaluation of the prototype on case studies in synthetic biology; and
- Predicate abstraction and SAT/SMT solving techniques for CTMC models.

The second position will investigate methodologies for rare-event
stochastic simulations. In particular, we are interested in investigating:
- Counterexample-guided importance sampling techniques;
- Prototype software implementation; and
- Benchmark stochastic computing circuits in nanotechnology.
========================================

Qualifications:
Applicants must have a bachelor's degree in Electrical/Computer
Engineering, Computer Science, or a related field. The successful candidate
is expected to demonstrate strong background and interest in formal methods
and algorithms, and preferably basic knowledge of probability and random
process. She/He should be confident in independently developing academic
software tools. Good writing and presentation skills in English are
important as well. Knowledge of synthetic biology is preferred, but not
required.
========================================

Salary:
This is a fully paid position. The successful PhD candidate receives $1,600
per month. The pay is negotiable. The candidate is expected to work on
average 20 hours per week during fall and spring semesters, and up to 40
hours per week during the summer. As a graduate student, you will receive a
full tuition waiver. Additionally, you will receive student insurance
coverage. Depending on funding situation, tuition differential and fees may
also be covered.
========================================

ECE Department at USU:
The place of employment is the Electrical and Computer Engineering
Department at Utah State University. The main campus is located in Logan,
Utah, 88 miles (about 142 km) north of Salt Lake City. The mission of the
Department of Electrical and Computer Engineering is to serve society
through excellence in learning, discovery, and outreach. We provide
undergraduate and graduate students an education in electrical and computer
engineering, and we aspire to instill in them attitudes, values, and
visions that will prepare them for lifetimes of continued learning and
leadership in their chosen careers. Through research, the department
strives to generate and disseminate new knowledge and technology for the
benefit of the State of Utah, the nation, and beyond. The detailed graduate
program description can be found at:
https://engineering.usu.edu/ece/students/graduate/index.Graduate
application information is available at:
https://engineering.usu.edu/ece/files/pdfs/ece-graduate-program-application-info.pdf
.
========================================

Additional Information about Logan:Logan is a valley community of about
125,000 people nestled in between the Wellsville Mountains and Bear River
Range in northeastern Utah. The many ski resorts, lakes, rivers, and
mountains in the region make it one of the finest outdoor recreation
environments in the nation. With views of a natural area reserve from
campus, the pristine natural environment of the area makes Logan one of
America's most attractive and affordable university towns (
https://www.explorelogan.com/).
========================================

Contact:
For questions about this position, please contact: Dr. Zhen Zhang (
zhen.zhang@usu.edu) and Dr. Chris Winstead (chris.winstead@usu.edu).

**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************