IEEE Organizations related to Model Checking

Back to Top

No organizations are currently tagged "Model Checking"



Conferences related to Model Checking

Back to Top

2020 IEEE/ACM 42nd International Conference on Software Engineering (ICSE)

ICSE is the premier forum for researchers to present and discuss the most recent innovations,trends, outcomes, experiences, and challenges in the field of software engineering. The scopeis broad and includes all original and unpublished results of empirical, conceptual, experimental,and theoretical software engineering research.


2019 21st International Conference on Advanced Communication Technology (ICACT)

With technically co-sponsored by IEEE ComSoc(Communications Society), IEEE ComSocCISTC(Communications & Information Security Technical Community), and IEEE ComSocONTC(Optical Networking Technical Community), the ICACT(International Conference onAdvanced Communications Technology) Conference has been providing an open forum forscholars, researchers, and engineers to the extensive exchange of information on newlyemerging technologies, standards, services, and applications in the area of the advancedcommunications technology. The conference official language is English. All the presentedpapers have been published in the Conference Proceedings, and posted on the ICACT Websiteand IEEE Xplore Digital Library since 2004. The honorable ICACT Out-Standing Paper Awardlist has been posted on the IEEE Xplore Digital Library also, and all the Out-Standing papersare subjected to the invited paper of the "ICACT Transactions on the Advanced Communications Technology" Journal issue by GIRI

  • 2018 20th International Conference on Advanced Communication Technology (ICACT)

    With technically co-sponsored by IEEE ComSoc(Communications Society), IEEE ComSoc CISTC(Communications & Information Security Technical Community), and IEEE ComSoc ONTC(Optical Networking Technical Community), the ICACT(International Conference on Advanced Communications Technology) Conference has been providing an open forum for scholars, researchers, and engineers to the extensive exchange of information on newly emerging technologies, standards, services, and applications in the area of the advanced communications technology. The conference official language is English. All the presented papers have been published in the Conference Proceedings, and posted on the ICACT Website and IEEE Xplore Digital Library since 2004. The honorable ICACT Out-Standing Paper Award list has been posted on the IEEE Xplore Digital Library also, and all the Out-Standing papers are subjected to the invited paper of the "ICACT Transactions on the Advanced Communications Technology" Journal issued by GIRI

  • 2017 19th International Conference on Advanced Communication Technology (ICACT)

    With technically co-sponsored by IEEE ComSoc(Communications Society), IEEE ComSoc CISTC(Communications & Information Security Technical Community), and IEEE ComSoc ONTC(Optical Networking Technical Community), the ICACT(International Conference on Advanced Communications Technology) Conference has been providing an open forum for scholars, researchers, and engineers to the extensive exchange of information on newly emerging technologies, standards, services, and applications in the area of the advanced communications technology. The conference official language is English. All the presented papers have been published in the Conference Proceedings, and posted on the ICACT Website and IEEE Xplore Digital Library since 2004. The honorable ICACT Out-Standing Paper Award list has been posted on the IEEE Xplore Digital Library also, and all the Out-Standing papers are subjected to the invited paper of the "ICACT Transactions on the Advanced Communications Technology" Journal issued by

  • 2016 18th International Conference on Advanced Communication Technology (ICACT)

    With technically co-sponsored by IEEE ComSoc(Communications Society), IEEE ComSoc CISTC(Communications & Information Security Technical Community), and IEEE ComSoc ONTC(Optical Networking Technical Community), the ICACT(International Conference on Advanced Communications Technology) Conference has been providing an open forum for scholars, researchers, and engineers to the extensive exchange of information on newly emerging technologies, standards, services, and applications in the area of the advanced communications technology. The conference official language is English. All the presented papers have been published in the Conference Proceedings, and posted on the ICACT Website and IEEE Xplore Digital Library since 2004. The honorable ICACT Out-Standing Paper Award list has been posted on the IEEE Xplore Digital Library also, and all the Out-Standing papers are subjected to the invited paper of the "ICACT Transactions on the Advanced Communications Technology" Journal issued by GiRI.

  • 2015 17th International Conference on Advanced Communication Technology (ICACT)

    With technically co-sponsored by IEEE ComSoc(Communications Society), IEEE ComSoc CISTC(Communications & Information Security Technical Community), and IEEE ComSoc ONTC(Optical Networking Technical Community), the ICACT(International Conference on Advanced Communications Technology) Conference has been providing an open forum for scholars, researchers, and engineers to the extensive exchange of information on newly emerging technologies, standards, services, and applications in the area of the advanced communications technology. The conference official language is English. All the presented papers have been published in the Conference Proceedings, and posted on the ICACT Website and IEEE Xplore Digital Library since 2004. The honorable ICACT Out-Standing Paper Award list has been posted on the IEEE Xplore Digital Library also, and all the Out-Standing papers are subjected to the invited paper of the "ICACT Transactions on the Advanced Communications Technology" Journal issued by GiRI.

  • 2014 16th International Conference on Advanced Communication Technology (ICACT)

    Technology, service, architecture, strategy, and policy in newly emerging system, standard, service, and variety of application on the area of telecommunications. ICACT 2014 provides an open forum for scholar, researcher, engineer, policy maker, network planner, and service provider in the advanced communication technologies.

  • 2013 15th International Conference on Advanced Communication Technology (ICACT)

    Technology, standard, service, architecture, strategy, and policy in newly emerging systems and a variety of applications in the area of communications. ICACT2013 provides an open forum for scholar, researcher, engineer, policy maker, network planner, and service provider in the advanced communications technologies.

  • 2012 14th International Conference on Advanced Communication Technology (ICACT)

    Technology, service, architecture, strategy, and policy in newly emerging systems, standards, service, and a variety of applications in the area of telecommunicatons. ICACT 2012 provides an open forum for scholars, researchers, engineers, policy makers, network planners, and service providers in the advanced communication technologies.

  • 2011 13th International Conference on Advanced Communication Technology (ICACT)

    International Conference on Advanced Communication Technology (ICACT) provides an open forum for researchers, engineers, policy, network planners, and service providers in the advanced communication technologies. Extensive exchange of information will be provided on newly emerging systems, standards, services, and variety of applications on the area of telecommunications.

  • 2010 12th International Conference on Advanced Communication Technology (ICACT)

    ICACT is an annual conference providing an open forum for researchers, engineers, network planners, and service providers in telecommunications. Extensive exchange of information will be provided on newly emerging systems, standards, services, and variety of applications in the area of telecommunications.

  • 2009 11th International Conference on Advanced Communication Technology (ICACT)

    ICACT is an annual conference providing an open forum for researchers, engineers, network planners, and service providers in telecommunications. Extensive exchange of information will be provided on newly emerging systems, standards, services, and variety of applications in the area of telecommunications.

  • 2008 10th International Conference Advanced Communication Technology (ICACT)

  • 2007 9th International Conference Advanced Communication Technology (ICACT)

  • 2006 8th International Conference Advanced Communication Technology (ICACT)

  • 2005 7th International Conference Advanced Communication Technology (ICACT)

  • 2004 6th International Conference Advanced Communication Technology (ICACT)


2019 32nd International Conference on VLSI Design and 2019 18th International Conference on Embedded Systems (VLSID)

This conference is a forum for researchers and designers to present and discuss variousaspects of VLSI design, EDA, embedded systems, and enabling technologies. The program willconsist of regular paper sessions, special sessions, embedded tutorials, panel discussions,design contest, industrial exhibits and tutorials. This is the premier conference/exhibition in thisarea in India, attracting designers, EDA professionals, and EDA tool users. The programcommittee for the conference has a significant representation from the EDA researchcommunity and a large fraction of the papers published in this conference are EDA-related


2019 IEEE 23rd International Conference on Computer Supported Cooperative Work in Design (CSCWD)

Collaboration technologies and applications to the design of processes, products, systems, and services in industries and societies. Application domains include aerospace, automotive, manufacturing, construction, logistics, transportation, power and energy, healthcare, infrastructure, administration, social networks, and entertainment.


2019 IEEE 49th International Symposium on Multiple-Valued Logic (ISMVL)

Multiple-Valued Logic has many aspects. This yearly event attracts researchers in this area.

  • 2018 IEEE 48th International Symposium on Multiple-Valued Logic (ISMVL)

    The Conference will bring together researchers from computer science, engineering, mathematics, and further disciplines to discuss new developments and directions for future research in the area of multi-valued logic and related fields. Research papers, surveys, or tutorial papers on any subject in these areas are within the scope of the symposium.

  • 2017 IEEE 47th International Symposium on Multiple-Valued Logic (ISMVL)

    The symposium encompasses all aspects of multiple-valued logic and application.

  • 2016 IEEE 46th International Symposium on Multiple-Valued Logic (ISMVL)

    Multiple-valued logic (MVL) is the study of circuits, oftware, architectures, and systems in which information is carried by more than two values, or where information is presented in unconventional, i.e., non-binary-weighted ways. The scope of ISMVL covers a broad range of related topics, including fundamental algebra, theory and philosophy, logic synthesis, decision diagrams, reversible computing, quantum computing, microelectronic circuits, testing andverification, architectures, and modelling of novel devices, all within a multiple-valued framework.

  • 2015 IEEE International Symposium on Multiple-Valued Logic (ISMVL)

    Multiple-valued logic (MVL) is the study of circuits, software, architectures, and systems in which information is carried by more than two values, or where information is represented in unconventional, i.e., non-binary-weighted ways. The scope of ISMVL covers a broad range of related topics, including fundamental algebra, theory and philosophy, logic synthesis, decision diagrams, reversible computing, quantum computing, microelectronic circuits, testing and verification, architectures, and modelling of novel devices, all within a multiple-valued framework.

  • 2014 IEEE 44th International Symposium on Multiple-Valued Logic (ISMVL)

    The aim of the conference is to present and disseminate knowledge in the areas related to multiple-valued logic, that is, to computing that is tolerant of imprecision, uncertainty, partial truth, and approximative reasoning. Specific topics include (but are not limited to):- Algebra and Formal Aspects- Automatic Test Pattern Generation- Automatic Reasoning- Boolean Satisfiability- Circuit/Device Implementation- Communication Systems- Computer Arithmetic- Data Mining- Fuzzy Systems and Soft Computing- Image Processing- Logic Design and Switching Theory- Logic Programming- Machine Learning and Robotics- Mathematical Fuzzy Logic- Nanotechnology- Philosophical Aspects- Quantum Computing- Quantum Cryptography- Reversible Computation- Signal Processing- Spectral Techniques- Verification

  • 2013 IEEE 43rd International Symposium on Multiple-Valued Logic (ISMVL)

    ISMVL is the principal annual meeting for the dissemination and discussion of research in multiple-valued logic and related areas. Topics cover all aspects of theory, implementation and application.

  • 2012 IEEE 42nd International Symposium on Multiple-Valued Logic (ISMVL)

    ISMVL is the principal annual meeting for the dissemination and discussion of research in multiple-valued logic and related areas. Topics cover all aspects of theory, implementation and application.

  • 2011 IEEE 41st International Symposium on Multiple-Valued Logic (ISMVL)

    areas of multiple-valued logic, including but not limited to: Algebra and Formal Aspects, ATPG and SAT, Automatic Reasoning, Circuit/Device Implementation, Communication Systems, Computer Arithmetic, Data Mining, Fuzzy Systems and Soft Computing, Image Processing, Logic Design and Switching Theory, Logic Programming Machine Learning and Robotics, Mathematical Fuzzy Logic, Nano Technology, Philosophical Aspects Quantum Computing, Signal Processing, Spectral Techniques, Verification.

  • 2010 40th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2010)

    The Multiple-Valued Logic Technical Committee of the IEEE Computer Society will hold its 40th annual symposium on May 26-28, 2010 in Casa Convalesc ncia, Barcelona, Spain. The event is sponsored by the IEEE Computer Society, and is organized by the Artificial Intelligence Research Institute of the Spanish National Research Council (IIIA-CSIC), the University of Barcelona, the Autonomous University of Barcelona, and the University of Lleida.

  • 2009 39th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2009)

    The area of multiple-valued logic is covered, including but not limited to: Algebra and Formal Aspects, Automatic Reasoning, Logic Programming, Philosophical Aspects, Fuzzy Logic and Soft Computing, Data Mining, Machine Learning and Robotics, Quantum Computing, Logic Design and Switching Theory, Test and Verification, Spectral Techniques, Circuit/Device Implementation, VLSI Architecture, VLSI Computing, System-on-Chip Technology, Nano Technology.

  • 2008 38th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2008)

    The aim of ISMVL is to publish and disseminate knowledge in the field of multiple-valued logic and related areas. All aspects of MVL are considered at the symposium, ranging form algebra, formal aspects, and philosophy to logic design, verification, and circuit implementation.

  • 2007 37th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2007)

  • 2006 36th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2006)

  • 2005 35th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2005)


More Conferences

Periodicals related to Model Checking

Back to Top

No periodicals are currently tagged "Model Checking"


Most published Xplore authors for Model Checking

Back to Top

Xplore Articles related to Model Checking

Back to Top

Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude

Assured Cloud Computing, None

To deal with large amounts of data while offering high availability, throughput, and low latency, cloud computing systems rely on distributed, partitioned, and replicated data stores. Such cloud storage systems are complex software artifacts that are very hard to design and analyze. We argue that formal specification and model checking analysis should significantly improve their design and validation. In particular, ...


Poster: Static Analysis of Concurrent Higher-Order Programs

2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, 2015

Few static analyses support concurrent higher-order programs. Tools for detecting concurrency bugs such as deadlocks and race conditions are nonetheless invaluable to developers. Concurrency can be implemented using a variety of models, each supported by different synchronization primitives. Using this poster, we present an approach for analyzing concurrent higher- order programs in a precise manner through abstract interpretation. We instantiate ...


On supervisor synthesis theorem and its application to embedded systems

2017 IEEE International Symposium on Consumer Electronics (ISCE), 2017

Embedded systems must be improved to survive in the rapid-changing business environment. Supervisory control is a promising approach for such improvement. This paper presented the introduction of supervisory control theory to embedded systems. The major results are (i) a theorem for supervisory control and (ii) its property which enables us to apply model checking technique to the analysis of the ...


On service personalization analysis for the internet of me based on PN2

2016 IEEE International Conference on Consumer Electronics (ICCE), 2016

In this paper, we proposed an approach for modeling services and service personalization based on a formal tool called PN2 (Petri nets in a Petri net). We showed that an Internet of Me (IoM for short) environment can be modeled with PN2. Then, we proposed a method to verify service personalization of a PN2 model. We illustrated the proposed method ...


Towards Model Checking-Driven Fair Comparison of Dynamic Thermal Management Techniques under Multi-Threaded Workloads

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, None

Dynamic thermal management (DTM) techniques are being widely used for attenuation of thermal hot spots in many-core systems. Conventionally, DTM techniques are analyzed using simulation and emulation methods, which are in- exhaustive due to their inherent limitations and cannot provide for a comprehensive comparison between DTM techniques owing to the wide range of corresponding design parameters. In order to handle ...


More Xplore Articles

Educational Resources on Model Checking

Back to Top

IEEE-USA E-Books

  • Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude

    To deal with large amounts of data while offering high availability, throughput, and low latency, cloud computing systems rely on distributed, partitioned, and replicated data stores. Such cloud storage systems are complex software artifacts that are very hard to design and analyze. We argue that formal specification and model checking analysis should significantly improve their design and validation. In particular, we propose rewriting logic and its accompanying Maude tools as a suitable framework for formally specifying and analyzing both the correctness and the performance of cloud storage systems. This chapter largely focuses on how we have used rewriting logic to model and analyze industrial cloud storage systems such as Google's Megastore, Apache Cassandra, Apache ZooKeeper, and RAMP. We also touch on the use of formal methods at Amazon Web Services.

  • Poster: Static Analysis of Concurrent Higher-Order Programs

    Few static analyses support concurrent higher-order programs. Tools for detecting concurrency bugs such as deadlocks and race conditions are nonetheless invaluable to developers. Concurrency can be implemented using a variety of models, each supported by different synchronization primitives. Using this poster, we present an approach for analyzing concurrent higher- order programs in a precise manner through abstract interpretation. We instantiate the approach for two static analyses that are capable of detecting deadlocks and race conditions in programs that rely either on compare-and-swap (cas), or on conventional locks for synchronization. We observe few false positives and false negatives on a corpus of small concurrent programs, with better results for the lock-based analyses. We also observe that these programs lead to a smaller state space to be explored by the analyses. Our results show that the choice of synchronization primitives supported by an abstract interpreter has an important impact on the complexity of the static analyses performed with this abstract interpreter.

  • On supervisor synthesis theorem and its application to embedded systems

    Embedded systems must be improved to survive in the rapid-changing business environment. Supervisory control is a promising approach for such improvement. This paper presented the introduction of supervisory control theory to embedded systems. The major results are (i) a theorem for supervisory control and (ii) its property which enables us to apply model checking technique to the analysis of the model given by the theorem. They were illustrated with an example of car controller.

  • On service personalization analysis for the internet of me based on PN2

    In this paper, we proposed an approach for modeling services and service personalization based on a formal tool called PN2 (Petri nets in a Petri net). We showed that an Internet of Me (IoM for short) environment can be modeled with PN2. Then, we proposed a method to verify service personalization of a PN2 model. We illustrated the proposed method with an example of an IoM environment and its service personalization.

  • Towards Model Checking-Driven Fair Comparison of Dynamic Thermal Management Techniques under Multi-Threaded Workloads

    Dynamic thermal management (DTM) techniques are being widely used for attenuation of thermal hot spots in many-core systems. Conventionally, DTM techniques are analyzed using simulation and emulation methods, which are in- exhaustive due to their inherent limitations and cannot provide for a comprehensive comparison between DTM techniques owing to the wide range of corresponding design parameters. In order to handle the above discrepancies, we propose to use model checking, a state-space based formal method, to model, evaluate and compare DTM techniques across various functional and performance parameters. The suggested framework includes a modeling flow and a set of generic modules that realistically model many-core and DTM parameters like temperature, power, application, inter-core communication and task migration etc. For analysis purpose, the framework provides a common ground for comparing DTM techniques by formalizing DTM principles and performance parameters as a set of logical properties. These properties are verified for different task load configurations, e.g., multi-threaded, malleable, and the applications which do not support migration. We analyze state-of-the-art central (c-) and distributed (d-) DTM techniques to demonstrate the generality and efficacy of our approach. Our formal analysis shows that the state-of-the- art cDTM technique performs better than dDTM in terms of achieving thermal stability, task migration and communication overhead. We believe that conventional analysis methods do not facilitate such an exhaustive comparison among the DTM techniques.

  • Development of SMT-Based Bounded Model Checker for embedded assembly program

    Recently, embedded assembly programs have properties dependent on hardware (direct operation of address spaces, memory mapped I/O, interruption, etc.) in the process of development. Thus, demands about the established method of formal verifications corresponding to those properties are increasing from the point of view of shorter development and high reliability. Our work aims at enabling formal verification for embedded software. We propose the detailed verification method with SMT-Based BMC for the Assembly Code Block (ACB). In addition, we have developed the automatic verification. Our method is based on the verification for the assembly program [1] and the verification using SMT- Based BMC for the embedded ANSI-C program [2] [3]. In this paper, we have developed the parser and the model converter for source codes of assembly program (assembly codes). Moreover, we show the validity of our method by experiments.

  • Hardware model checking competition 2017

    The Hardware Model Checking Competition (HWMCC) 2017 affiliated to the International Conference on Formal Methods in Computer Aided Design (FMCAD) in 2017 in Vienna was the 9th competitive event for hardware model checkers we organized. After HWMCC'15 affiliated with FMCAD'15 in Austin, the competition took a break in 2016.

  • Similarity-Based Search for Model Checking: A Pilot Study with Java PathFinder

    When a model checker cannot explore the entire state space because of limited resources, model checking becomes a kind of testing with an attempt to find a failure (violation of properties) quickly. We consider two state sequences in model checking: (i) the sequence in which new states are generated, and (ii) the sequence in which the states generated in sequence (i) are checked for property violation. We observe that neighboring states in sequence (i) often have similarities in certain ways. Based on this observation we propose a search strategy, which generates sequence (ii) in such a way that similar states are evenly spread over the sequence. As a result, neighboring states in sequence (ii) can have a higher diversity. A pilot empirical study with Java Path Finder suggests that the proposed strategy can outperform random search in terms of creating equal or smaller number of states to detect a failure.

  • Model Checking PBFT Consensus Mechanism in Healthcare Blockchain Network

    Now blockchain network is used in many areas such as healthcare, energy trading and so on. However, the research about how to evaluate the performance of the blockchain network is insufficient. In some papers, the performance of blockchain is analyzed by running real blockchain applications. However, the devices and services cost is a burden. In this paper, we aim to use continuous-time Markov chain (CTMC) models to simulate the time response of PBFT (Practical Byzantine Fault Tolerance)-based healthcare blockchain network. Some influencing factors such as replica nodes delay and primary node delay will be analyzed. The simulation results also contribute to the optimization design of blockchain network.

  • Reducing CTL-live model checking to first-order logic validity checking

    Temporal logic model checking of infinite state systems without the use of iteration or abstraction is usually considered beyond the realm of first-order logic (FOL) reasoners because of the need for a fixpoint computation. In this paper, we show that it is possible to reduce model checking of a finite or infinite Kripke structure that is expressed in FOL to a validity problem in FOL for a fragment of computational tree logic (CTL), which we call CTL-live. CTL-live includes the CTL connectives that are traditionally used to express liveness properties. Our reduction can form the basis for methods that use FOL reasoning techniques directly to accomplish model checking of CTL-live properties without the need for fixpoint operators, transitive closure, abstraction, or induction.



Standards related to Model Checking

Back to Top

No standards are currently tagged "Model Checking"


Jobs related to Model Checking

Back to Top