Automated test generation and error localisation for Simulink/Stateflow modelled systems using extended automata by Meng Li, Ratnesh Kumar

Subjects: Get full text

Verification using counterexample fragment based specification relaxation: case of modular/concurrent linear hybrid automata by Hao Ren, Jing Huang, Jing Huang, Shengbing Jiang, Ratnesh Kumar

Subjects: “…formal verification…”
Get full text

Custom Integrated Circuits by Allen, Jonathan, Wyatt, John L., Jr., White, Jacob K., Devadas, Srinivas, Armstrong, Robert C., Baltus, Donald G., Pickelsimer, Lisa A., Reichelt, Mark W., Van Aelten, Filip J., Horn, Berthold K. P., Lee, Hae-Seung, Sodini, Charles G., Poggio, Tomaso, Decker, Steven J., Dron, Lisa G., Elfadel, Ibrahim M., Eshghi, Kamyar, Hakkarainen, Mikko, Harris, John G., Herrmann, Frederick P., Keast, Craig L., Martin, David R., McQuirk, Ignacio S., Seidel, Mark N., Standley, David L., Thompson, Clay M., Umminger, Christopher B., Yu, Paul C., Lumsdaine, Andrew, Silveira, Luis M., Leeb, Steve B., Lloyd, Jennifer A., Rahmat, Khalid, Antoniadis, Dimitri A., Nabors, Keith S., Kim, Songmin, Ali, Sami M., Telichevsky, Ricardo, Dally, William J., Kamon, Mattan, Schmidt, Martin A., Senturia, Stephen D., Kukula, James H., Bai, Kelly S., Liao, Stan Y., Shen, Amelia H.

Subjects: Get full text

Custom Integrated Circuits by Allen, Jonathan, Wyatt, John L., Jr., White, Jacob K., Devadas, Srinivas, Armstrong, Robert C., Baltus, Donald G., Pickelsimer, Lisa A., Reichelt, Mark W., Tan, Chin Hwee, Van Aelten, Filip J., Horn, Berthold K. P., Lee, Hae-Seung, Masaki, Ichiro, Sodini, Charles G., Lumsdaine, Andrew, Rahmat, Khalid, Antoniadis, Dimitri A., Silveira, Luis M., Leeb, Steven B., Telichevsky, Ricardo, Dally, William J., Cai, Xuejun, Kamon, Mattan, Schmidt, Martin A., Senturia, Stephen D., Phillips, Joel R., van der Zant, Herre S. J., Orlando, Terry P., Kim, Songmin, Nabors, Keith S., Alidina, Mazhar M., Bhagwati, Vishal L., Bai, Kelly S., Liao, Stan Y., Monteiro, Jose C., Shen, Amelia H.

Subjects: Get full text

Formal Specification and Verification of Self-Adaptive Concurrent Systems by Muhammad Ilyas Fakhir, Syed Asad Raza Kazmi

Subjects: Get full text

Custom Integrated Circuits by Allen, Jonathan, Wyatt, John L., Jr., White, Jacob K., Devadas, Srinivas, Armstrong, Robert C., Baltus, Donald G., McDonald, Robert G., Tan, Chin Hwee, Horn, Berthold K. P., Lee, Hae-Seung, Sodini, Charles G., Keast, Craig L., Masaki, Ichiro, Decker, Steven J., Dron, Lisa G., Elfadel, Ibrahim M., Hakkarainen, J. Mikko, Herrmann, Frederick P., Martin, David R., McQuirk, Ignacio S., Reichelt, Mark W., Seidel, Mark N., Silveira, Luis M., Umminger, Christopher B., Yu, Paul C., Lumsdaine, Andrew, Rahmat, Khalid, Antoniadis, Dimitri A., Cai, Xuejun, Kamon, Mattan, Yie, He, Schmidt, Martin A., Senturia, Stephen D., Phillips, Joel R., van der Zant, Herre S. J., Orlando, Terry P., Kim, Songmin, Nabors, Keith S., Chou, Michael T., Korsmeyer, F. Thomas, Leeb, Steven B., Alidina, Mazhar M., Bhagwati, Vishal L., Liao, Stan Y., Monteiro, José C., Rinderknecht, W. John, Shen, Amelia H.

Subjects: Get full text

Verification of tree-based hierarchical read-copy update in the Linux kernel by Liang, L, McKenney, PE, Kroening, D, Melham, TF

“…This suggests use of formal verification. Previous formal verification efforts for RCU either focus on simple implementations or use modeling languages. …”

An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Project by Frank Dordowsky

“…Safety critical avionics software is a natural application area for formal verification. This is reflected in the formal method's inclusion into the certification guideline DO-178C and its formal methods supplement DO-333. …”
Get full text

Architecture of the Formally-Verified Distributed Ledger System InnoChain by Leonid Al'bertovich Merkin-Janson, Ruslan Maratovich Rezin, Nikolay Konstantinovich Vasilyev

“…In this paper we consider the software architecture of InnoChain, a distributed ledger system (DLS) with 5 levels of formal verification, including a formally-verified underlying operating system (OS). …”
Get full text

A statistical approach to assessing neural network robustness by Webb, S, Rainforth, T, Teh, Y, Mudigonda, P

“…Our approach critically varies from the formal verification framework in that when the property can be violated, it provides an informative notion of how robust the network is, rather than just the conventional assertion that the network is not verifiable. …”

Analyzing model checking approach for multi agent system verification by Selamat, Ali, Abu Bakar, Najwa

“…Therefore, in this paper, we present our studies of formal verification of multi agent system using model checking approach. …”

Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models by Peter Csaba Ölveczky, Kyungmin Bae

“…The synthesis of a Real-Time Maude verification model from a Ptolemy II DE model, and the formal verification of the synthesized model in Real-Time Maude, have been integrated into Ptolemy II, enabling a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude.…”
Get full text

Verification of Transaction Level Models of Embedded Systems by Lucky Lochi Yu Lo

“…In order to shorten this verification phase of the design, we propose a methodology to do formal verification of embedded systems. In formal verification no test cases are needed, but an mathematical analysis of the original model and the refined one. …”
Get full text

Verification of SpecC using predicate abstraction. by Clarke, E, Jain, H, Kroening, D

“…Languages such as SystemC or SpecC offer modeling of hardware and whole system designs at a high level of abstraction. However, formal verification techniques are widely applied in the hardware design industry only for low level designs, such as a netlist or RTL. …”

Specification and Verification of Context-dependent Services by Naseem Ibrahim, Vangalur Alagar, Mubarak Mohammad

“…Without a formal basis it is not possible to justify through formal verification the correctness conditions for service compositions and the satisfaction of contractual obligations in service provisions. …”
Get full text

Trustworthy Refactoring via Decomposition and Schemes: A Complex Case Study by Dániel Horpácsi, Judit Kőszegi, Zoltán Horváth

“…Widely used complex code refactoring tools lack a solid reasoning about the correctness of the transformations they implement, whilst interest in proven correct refactoring is ever increasing as only formal verification can provide true confidence in applying tool-automated refactoring to industrial-scale code. …”
Get full text

Synthesis and verification of delf-aware computing systems by Calinescu, R, Autili, M, Camara, J, Di Marco, A, Gerasimou, S, Inverardi, P, Perucci, A, Jansen, N, Katoen, J, Kwiatkowska, M, Mengshoel, O, Spalazzese, R, Tivoli, M

“…This chapter describes two classes of key enabling techniques for self-adaptive systems: automated synthesis and formal verification. The ability to dynamically synthesize component connectors and compositions underpins the proactive adaptation of the architecture of self-aware systems. …”

Pengujian Ketentuan Penghapusan Norma dalam Undang-Undang by Muchamad Ali Safa’at

“… Theoretically and practically (judicial review), include two types, namely formal verification (formale toetsingrecht) and material verification (materielle toetsingrecht). …”
Get full text

Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using SMT Solvers by Bence Czipó, Ákos Hajdu, Tamás Tóth, István Majzik

“…Statecharts are frequently used as a modeling formalism in the design of state-based systems. Formal verification techniques are also often applied to prove certain properties about the behavior of the system. …”
Get full text

A Formal Model For Real-Time Parallel Computation by Peter Hui, Satish Chikkagoudar

“…The imposition of real-time constraints on a parallel computing environment– specifically high-performance, cluster-computing systems– introduces a variety of challenges with respect to the formal verification of the system's timing properties. In this paper, we briefly motivate the need for such a system, and we introduce an automaton-based method for performing such formal verification. …”
Get full text