Page 60 - 2017 Brochure
P. 60
究員
王柏堯 Bow-Yaw Wang
Research Fellow
Ph.D., Computer Science, University of Pennsylvania
Tel: +886-2-2788-3799 ext. 1717 Fax: +886-2-2782-4814
Email: bywang@iis.sinica.edu.tw
http://www.iis.sinica.edu.tw/~bywang
• Research Fellow, Institute of Information Science, Academia Sinica (2012-present)
• Associate Research Fellow, Institute of Information Science, Academia Sinica (2008-2012)
• Associate Professor (Adjoint), National Taiwan University (2009-2012)
• Invited Professor, INRIA, France (2009-2011)
• Assistant Research Fellow, Institute of Information Science, Academia Sinica (2003-2008)
• Invited Associate Professor, Tsinghua University, China (2009-2010)
• Assistant Professor (Adjoint), National Taiwan University (2004-2009)
• Senior Software Engineer, Verplex Systems (2001-2003)
Research Description safety property, however, system design expertise is required to
identify relevant system components. Additionally, for systems
My research interests include computational logic, automata theory with complicated interactions among components, identifying
and formal verification, especially including model checking. Formal the relevant system components can be very time consuming.
verification is a mathematical and logical method that checks Algorithmic learning has been used to infer this information for
properties about computer systems. Among several techniques in verification tasks. It was first used to synthesize explicit system
formal verification, I am most interested in model checking. Given a components, however, we are now able to extend its application to
formal property and a system description, a model checker verifies infer implicit system models and even probabilistic models.
whether the system description conforms to the property. The
model checking problem, in general, is computationally difficult, Another focus of my research is to apply formal verification to
and therefore I have been developing algorithms and heuristics to practical cryptography. Modern cryptography such as Elliptic
improve efficiency. In order to evaluate the effectiveness of verification Curve Cryptography requires computation over large finite fields.
algorithms, I have implemented the model checker BASAI. This Commodity computing devices, however, do not support arithmetic
model checker supports both BDD- and SAT-based algorithms, and computation on 255-bit integers, for example. Hence, arithmetic
employs the Property Directed Reachability algorithm. over large finite fields needs to be implemented with 64- or 32-bit
In recent years, my research interests have focused on applying machine instructions. If such implementations are incorrect, any
algorithmic learning to formal verification. Consider, for instance, security guarantees of cryptosystems would be lost. It is therefore
verifying a safety property on a system composed of several of utmost importance to formally verify cryptographic programs
components. Oftentimes, an engineer verifies different aspects deployed in computing devices. Along with my colleagues, we have
of the system individually. For each aspect, she specifies a safety successfully verified the Montgomery Ladder Step in Curve25519, a
property and checks whether the relevant system components secure elliptic curve over the finite field GF(2255-19).
work properly. Only a portion of the system is needed to verify the
6. Fei He, Xiaowei Gao, Bow-Yaw Wang, and Lijun Zhang. Leveraging
Publications Weighted Automata in Compositional Reasoning about Concurrent
Probabilistic Systems. 42nd Annual ACM SIGPLAN-SIGACT
1. Fei He, Shu Mao, and Bow-Yaw Wang. Learning-based Assume- Symposium on Principles of Programming Languages (POPL 2015),
Guarantee Regression Verification. 28th International Conference on pp 503-514, 2015.
Computer Aided Verification (CAV 2016), Toronto, Ontario, Canada,
July 2016. 7. Yungbum Jung, Soonho Kong, Cristina David, Bow-Yaw Wang,
and Kwangkeun Yi. Automatically inferring loop invariants via
2. Yu-Fang Chen, Chiao Hsieh, Ondrej Lengal, Tsung-Ju Lii, Ming- algorithmic learning. Mathematical Structures in Computer Science
Hsien Tsai, Bow-Yaw Wang, and Farn Wang. PAC Learning-Based 25(4): 892-915 (2015).
Verification and Model Synthesis. 38th International Conference on
Software Engineering (ICSE 2016), Austin, USA, May 2016. 8. Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe,
Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, and Shang-Yi
3. Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, and Yang. Verifying Curve25519 Software. 21st ACM Conference on
Lijun Zhang. Learning Weighted Assumptions for Compositional Computer and Communications Security (CCS 2014), pp 299-309,
Verification of Markov Decision Processes. ACM Transactions 2014.
Software Engineering and Methodology (TOSEM). 25(3): 21:1-21:39
(2016). 9. Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, and
Farn Wang. Verifying Recursive Programs Using Intraprocedural
4. Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, and Lijun Zhang. Analyzers. 21st International Symposium on Static Analysis (SAS
Counterexample-Guided Polynomial Loop Invariant Generation by 2014), pp 118-133, LNCS 8723, 2014.
Lagrange Interpolation 27th International Conference on Computer
Aided Verification (CAV 2015), pp 658-674, LNCS 9206, 2015. 10. Fei He, Bow-Yaw Wang, Liangze Yin, and Lei Zhu. Symbolic
Assume-Guarantee Reasoning through BDD Learning. 36th
5. Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang. International Conference on Software Engineering (ICSE 2014), pp
Commutativity of Reducers. 21st International Conference on Tools 1071-1082, 2014.
and Algorithms for the Construction and Analysis of Systems (TACAS
2015), pp 131-146, LNCS 9035, 2015.
58 研究人員 Research Faculty
王柏堯 Bow-Yaw Wang
Research Fellow
Ph.D., Computer Science, University of Pennsylvania
Tel: +886-2-2788-3799 ext. 1717 Fax: +886-2-2782-4814
Email: bywang@iis.sinica.edu.tw
http://www.iis.sinica.edu.tw/~bywang
• Research Fellow, Institute of Information Science, Academia Sinica (2012-present)
• Associate Research Fellow, Institute of Information Science, Academia Sinica (2008-2012)
• Associate Professor (Adjoint), National Taiwan University (2009-2012)
• Invited Professor, INRIA, France (2009-2011)
• Assistant Research Fellow, Institute of Information Science, Academia Sinica (2003-2008)
• Invited Associate Professor, Tsinghua University, China (2009-2010)
• Assistant Professor (Adjoint), National Taiwan University (2004-2009)
• Senior Software Engineer, Verplex Systems (2001-2003)
Research Description safety property, however, system design expertise is required to
identify relevant system components. Additionally, for systems
My research interests include computational logic, automata theory with complicated interactions among components, identifying
and formal verification, especially including model checking. Formal the relevant system components can be very time consuming.
verification is a mathematical and logical method that checks Algorithmic learning has been used to infer this information for
properties about computer systems. Among several techniques in verification tasks. It was first used to synthesize explicit system
formal verification, I am most interested in model checking. Given a components, however, we are now able to extend its application to
formal property and a system description, a model checker verifies infer implicit system models and even probabilistic models.
whether the system description conforms to the property. The
model checking problem, in general, is computationally difficult, Another focus of my research is to apply formal verification to
and therefore I have been developing algorithms and heuristics to practical cryptography. Modern cryptography such as Elliptic
improve efficiency. In order to evaluate the effectiveness of verification Curve Cryptography requires computation over large finite fields.
algorithms, I have implemented the model checker BASAI. This Commodity computing devices, however, do not support arithmetic
model checker supports both BDD- and SAT-based algorithms, and computation on 255-bit integers, for example. Hence, arithmetic
employs the Property Directed Reachability algorithm. over large finite fields needs to be implemented with 64- or 32-bit
In recent years, my research interests have focused on applying machine instructions. If such implementations are incorrect, any
algorithmic learning to formal verification. Consider, for instance, security guarantees of cryptosystems would be lost. It is therefore
verifying a safety property on a system composed of several of utmost importance to formally verify cryptographic programs
components. Oftentimes, an engineer verifies different aspects deployed in computing devices. Along with my colleagues, we have
of the system individually. For each aspect, she specifies a safety successfully verified the Montgomery Ladder Step in Curve25519, a
property and checks whether the relevant system components secure elliptic curve over the finite field GF(2255-19).
work properly. Only a portion of the system is needed to verify the
6. Fei He, Xiaowei Gao, Bow-Yaw Wang, and Lijun Zhang. Leveraging
Publications Weighted Automata in Compositional Reasoning about Concurrent
Probabilistic Systems. 42nd Annual ACM SIGPLAN-SIGACT
1. Fei He, Shu Mao, and Bow-Yaw Wang. Learning-based Assume- Symposium on Principles of Programming Languages (POPL 2015),
Guarantee Regression Verification. 28th International Conference on pp 503-514, 2015.
Computer Aided Verification (CAV 2016), Toronto, Ontario, Canada,
July 2016. 7. Yungbum Jung, Soonho Kong, Cristina David, Bow-Yaw Wang,
and Kwangkeun Yi. Automatically inferring loop invariants via
2. Yu-Fang Chen, Chiao Hsieh, Ondrej Lengal, Tsung-Ju Lii, Ming- algorithmic learning. Mathematical Structures in Computer Science
Hsien Tsai, Bow-Yaw Wang, and Farn Wang. PAC Learning-Based 25(4): 892-915 (2015).
Verification and Model Synthesis. 38th International Conference on
Software Engineering (ICSE 2016), Austin, USA, May 2016. 8. Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe,
Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, and Shang-Yi
3. Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang, and Yang. Verifying Curve25519 Software. 21st ACM Conference on
Lijun Zhang. Learning Weighted Assumptions for Compositional Computer and Communications Security (CCS 2014), pp 299-309,
Verification of Markov Decision Processes. ACM Transactions 2014.
Software Engineering and Methodology (TOSEM). 25(3): 21:1-21:39
(2016). 9. Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, and
Farn Wang. Verifying Recursive Programs Using Intraprocedural
4. Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, and Lijun Zhang. Analyzers. 21st International Symposium on Static Analysis (SAS
Counterexample-Guided Polynomial Loop Invariant Generation by 2014), pp 118-133, LNCS 8723, 2014.
Lagrange Interpolation 27th International Conference on Computer
Aided Verification (CAV 2015), pp 658-674, LNCS 9206, 2015. 10. Fei He, Bow-Yaw Wang, Liangze Yin, and Lei Zhu. Symbolic
Assume-Guarantee Reasoning through BDD Learning. 36th
5. Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, and Bow-Yaw Wang. International Conference on Software Engineering (ICSE 2014), pp
Commutativity of Reducers. 21st International Conference on Tools 1071-1082, 2014.
and Algorithms for the Construction and Analysis of Systems (TACAS
2015), pp 131-146, LNCS 9035, 2015.
58 研究人員 Research Faculty
