| Concordia University,Montreal,Quebec, Canada | ||||||
| Ongoing | Asif Iqbal Ahmed | Gil Shapir | ||||
| RuleBase university program: support educational institutions in their verification-related education and research | ||||||
| Haifa University, Israel | ||||||
| Ongoing | Dr. Yaron Wolfsthal | Gil Shapir | ||||
|
Description of work: RuleBase university program: support educational institutions in their verification-related education and research | ||||||
| Haifa University, Israel | ||||||
| Ongoing | Yosi Ben-Asher | Eitan Farchi | ||||
| A Tool for Testing Multi-threaded Java Applications · Project Page | ||||||
| Pittsburgh University | ||||||
| Ongoing | Professor Steven P. Levitan | Gil Shapir | ||||
| RuleBase university program: support educational institutions in their verification-related education and research | ||||||
| Swiss Federal Institute of Technology Zurich (ETH) | ||||||
| Ongoing | Daniel Kroening | Karen Yorav | ||||
| Formal verification of software and improved bounded model checking techniques · Project Page | ||||||
| Technion - Israel Institute of Technology | ||||||
| Ongoing | Goel Samuel Prof. Orna Grumberg | Gil Shapir | ||||
| RuleBase university program: support educational institutions in their verification-related education and research | ||||||
| Technion - Israel Institute of Technology | ||||||
| Ongoing | Ofer Shtrichman | Roy Emek | ||||
| Finding well-distributed solutions to Constraint Satisfaction Problems (CSP). This work is done in the context of stimuli generation for functional verification of hardware designs. · Octopus | ||||||
| Technion - Israel Institute of Technology | ||||||
| Ongoing | Orna Grumberg | Ishai Rabinovitz | ||||
| Formal Verification | ||||||
| Tel Aviv University | ||||||
| Ongoing | Yishay Mansour | Shai Fine | ||||
| Hardware and Software Functional Verification using Machine Learning Techniques · Project Page | ||||||
| University of Bristol | ||||||
| Ongoing | Dr. Kerstin Eder | Michael Vinov | ||||
| The project is a Ph.D. research about coverage-directed-generation using machine-learning techniques. STMicroelectronics wishes to give the University its processor simulation and test generation environment as infrastructure needed to conduct the research. Genesys-Pro is part of this environment. | ||||||
| University of California Irvine | ||||||
| Ongoing | Ian G. Harris | Eyal Bin | ||||
| Constraint Satisfaction Problems (CSP) solvers and industrial benchmarks | ||||||
| University of Cambridge | ||||||
| Ongoing | Mike Gordon | Cindy Eisner | ||||
| A detailed machine readable semantics of PSL/Sugar has been developed in the version of higher order logic supported by the HOL system. Several sanity checking properties have been proved, including the equivalence of the clocked semantics with the composition of clock elimination rewrites followed by the unclocked semantics. The semantics in higher order logic is believed to be an accurate formalization of the semi-formal semantics in Appendix B of the Language Reference Manual. The semantics of PSL/Sugar is expected to change (e.g. modifications to the treatment of clocking and the semantics of aborts), but we expect to keep our machine readable semantics synchronized with the latest Accellera semantics. We list below some research projects that could build on the existing HOL semantics.
Machine readable golden semantics
Synthesizing checkers from PSL/Sugar
Validating translations between PSL/Sugar and other languages
Compiling very high level properties into PSL/Sugar
Verification using theorem proving
Investigating relations between PSL/Sugar and ITL
Further sanity checking · Project Page | ||||||
| University of North Carolina | ||||||
| Ongoing | Dr. John Goss | Gil Shapir | ||||
| RuleBase university program: support educational institutions in their verification-related education and research | ||||||
| Weizmann Institute of Science University URL: Description of work: University contact names: URLs of each university contact personal page: IBM contact Names: URLs of IBM contacts personal page: Project page link: Any other related link: http://www.prosyd.org/ | ||||||
| Ongoing | Dana Fisman | Cindy Eisner | ||||
| Basic research on the semantics of the temporal logic PSL/Sugar · Project Link · Related Link | ||||||
| Weizmann institute, Israel | ||||||
| Ongoing | Dr. Raya Leviathan | Gil Shapir | ||||
|
Description of work: RuleBase university program: support educational institutions in their verification-related education and research | ||||||