الصفحة 1
الصفحة 1
Verified Software: Theories, Tools, Experiments ; 1st IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions
The book includes a general introduction to the area, which also presents the vision of a grand challenge project: the "verifying compiler". Most contributions are followed by a transcription of the vivid discussion that ensued between the author and the audience. The papers have been organized in topical sections on verification tools, guaranteeing correctness, software engineering aspects, verifying object-oriented programming, programming language and methodology aspects, components, static analysis, design, analysis and tools, as well as formal techniques.
Verification, Model Checking, and Abstract Interpretation ; 3rd International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers
This volume contains the revised version of papers presented at VMCAI 2002,the Third International Workshop on Verification, Model Checking, and AbstractInterpretation, Venice (Italy), January 21-22, 2002.The main goal of the workshop was to give an overview of the main directionsdecisive for the growth and cross-fertilization of major research activities inprogram analysis and verification. The program committee selected 22 papers out of 41 submissions on the basisof at least 3 reviews. The resulting volume offers the reader an interesting perspectiveof the current research trends in the area. In particular, the papers contributeto the following topics: Security and Protocols, Timed Systems and Games,Static Analysis, Optimizations, Types and Verification, and Temporal Logicsand Systems.
Unifying Theories of Programming ; 1st International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006, Revised Selected Papers
A number of formal notations and theories have now emerged and proved them-selves effective as tools for the practisingsoftware engineer. Within these theorieswe see a number of common themes, such as abstraction, refinement, choice, ter-mination, feasibility, concurrency and communication. The commonality of suchthemes opens perspectives for unifying theories, an activity which can increaseour ability to use existing methods and notations, to recognise their limitations,and to extend and generalise them.
Unfoldings : A Partial-Order Approach to Model Checking
In this book the authors introduce unfoldings, an approach to model checking which alleviates the state explosion problem by means of concurrency theory. They offer a gentle introduction to the basics of the method, and in particular they detail an unfolding-based algorithm for model checking concurrent systems against properties specified as formulas of linear temporal logic (LTL). Self-contained chapters cover transition systems and their products; unfolding products; search procedures for basic verification problems, such as reachability and livelocks; and model checking LTL.
Understanding Programming Languages
This book is about describing the meaning of programming languages. While a compiler or an interpreter offers a form of formal description of a language, it is not something that can be used as a basis for reasoning about that language nor can it serve as a definition of a programming language itself since this must allow a range of implementations. By writing a formal semantics of a language a designer can yield a far shorter description and tease out, analyse and record design choices.Early in the book the author introduces a simple notation, a meta-language, used to record descriptions of the semantics of languages. In a practical approach, he considers dozens of issues that arise in current programming languages and the key techniques that must be mastered in order to write the required formal semantic descriptions. The book concludes with a discussion of the eight key challenges: delimiting a language (concrete representation), delimiting the abstract content of a language, recording semantics (deterministic languages), operational semantics (non-determinism), context dependency, modelling sharing, modelling concurrency, and modelling exits.
Transactions on Petri Nets and Other Models of Concurrency I
It contains teaching concurrency; process languages; process mining; software engineering; state space visualisation techniques; timed Petri nets; unfolding techniques and hardware systems. Thus, this volume gives a good overview of the state of the art in concurrency research.
Tools and Algorithms for the Construction and Analysis of Systems ; 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part II
This is Part II: concurrent and distributed systems; monitoring and runtime verification; hybrid and stochastic systems; synthesis; symbolic verification; and safety and fault-tolerant systems.
Tools and Algorithms for the Construction and Analysis of Systems ; 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II
The LNCS 10805 and 10806 proceedings set constitutes the proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018, which took place in Thessaloniki, Greece, in April 2018, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2018.The total of 43 full and 11 short papers presented in these volumes was carefully reviewed and selected from 154submissions. The papers are organized in topical sections as follows:Part I: theorem proving; SAT and SMT I; deductive verification; software verification and optimization; model checking; and machine learning.Part II: concurrent and distributed systems; SAT and SMT II; security and reactive systems; static and dynamic program analysis; hybrid and stochastic systems; temporal logic and mu-calculus; 7th Competition on Software Verification – SV-COMP.
Tools and algorithms for the construction and analysis of systems ; 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I
The LNCS 10805 and 10806 proceedings set constitutes the proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018, which took place in Thessaloniki, Greece, in April 2018, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2018.The total of 43 full and 11 short papers presented in these volumes was carefully reviewed and selected from 154submissions. The papers are organized in topical sections as follows:Part I: theorem proving; SAT and SMT I; deductive verification; software verification and optimization; model checking; and machine learning.Part II: concurrent and distributed systems; SAT and SMT II; security and reactive systems; static and dynamic program analysis; hybrid and stochastic systems; temporal logic and mu-calculus; 7th Competition on Software Verification – SV-COMP.
Tools and Algorithms for the Construction and Analysis of Systems ; 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings
The book is organized in topical sections on parameterized systems, model checking, applications, static analysis, concurrent/distributed systems, symbolic execution, abstraction, interpolation, trust, and reputation.
Theory and Practice of Model Transformations ; 1st International Conference, ICMT 2008, Zürich, Switzerland, July 1-2, 2008 Proceedings
This book includes different issues related with: process and engineering of model transformations; model transformations supporting concurrency and time; matching and mapping within model transformation rules; language support for model transformation reuse and modularity; and correctness and analysis of model transformations.
Theoretical Aspects of Computing - ICTAC 2006 ; 3rd International Colloquium, Tunis, Tunisia, November 20-24, 2006 Proceedings
Constitutes the refereed proceedings of the Third International Colloquium on Theoretical Aspects of Computing, ICTAC 2006 held in Tunis, Tunisia in November 2006. The 21 revised full papers presented together with three invited talks and summaries of two tutorials were carefully reviewed and selected from 78 submissions.
Theoretical Aspects of Computing - ICTAC 2004 ; 1st International Colloquium Guiyand, China, September 20-24, 2004, Revised Selected Papers
Constitutes the thoroughly refereed postproceedings of the First International Colloquium on Theoretical Aspects of Computing, ICTAC 2004. The 34 revised full papers presented together with 4 invited contributions were carefully selected from 111 submissions during two rounds of reviewing and improvement. The papers are organized in topical sections on concurrent and distributed systems, model integration and theory unification, program reasoning and testing, verification, theories of programming and programming languages, real-time and co-design, and automata theory and logics.
The Delft Systems Approach : Analysis and Design of Industrial Systems
The pace of development in knowledge and know-how in the fields of organisational sciences, logistics and information technology is rapid. However, the gap between the researcher in these areas and the practicing manager is growing. The Delft Systems Approach sets out to close the gap between theory and practic.
Testing of software and communicating systems ; 20th IFIP TC 6/WG 6.1 International Conference, TestCom 2008 8th International Workshop, FATES 2008 Tokyo, Japan, June 10-13, 2008 Proceedings
This book covers new approaches, concepts, theories, methodologies, tools, and experiences in the field of testing of communicating systems and general software. They are organized in topical sections on general software testing, testing continuous and real-time systems, network testing, test generation, concurrent system testing, and applications of testing.
Temporal Logic and State Systems
Temporal logic has developed over the last 30 years into a powerful formal setting for the specification and verification of state-based systems. Based on university lectures given by the authors, this book is a comprehensive, concise, uniform, up-to-date presentation of the theory and applications of linear and branching time temporal logic; TLA (Temporal Logic of Actions); automata theoretical connections; model checking; and related theories.
Systematic methodology for real-time cost-effective mapping of dynamic concurrent task-based systems on heterogeneous platforms
Systematic Methodology for Real-Time Cost-Effective Mapping of Dynamic Concurrent Task-Based Systems on Heterogeneous Platforms gives an overview of the state-of-the-art in system-level design trade-off explorations for concurrent tasks running on embedded heterogeneous multiple processors. The targeted application domain covers complex embedded real-time multi-media and communication applications.
Supervisory Control of Concurrent Systems : A Petri Net Structural Approach
Addresses the design of such tools for correct-by-construction synthesis of supervisors for systems and specifications represented in the discrete-event framework.
State of the Art for Minimally Invasive Spine Surgery
The contents of this book provide highly relevant and detailed information. I certainly believe that it will be a great bene?t to all orthopedic surgeons who are interested in performing minimally invasive spine surgery. Charoen Chotigavanich, M.D. Chairman, Spinal Section The Royal College of Orthopedic Surgeons of Thailand V Preface Recent decades have been characterized by revolutionary changes in spinal surgery. Concurrent progress in implant technology and functional en- scopes and the improvement of less invasive surgical techniques has opened a new dimension for spine surgery.
Software-Intensive Systems and New Computing Paradigms : Challenges and Visions
The objective was to imagine the landscape in which next generations of software-intensive systems will operate and the challenges they present to computing, software engineering, cognition and intelligence. The volume starts with an overview of the current state of the art and the research missions in engineering software-intensive systems. The book is structured in three major parts: ensemble engineering, theory and formal methods, and novel computing paradigms. These papers cover a broad spectrum of relevant topics ranging from methods, languages and tools for ensemble engineering, socio-technical and cyber-physical systems, ensembles in urban environments, formal methods and mathematical foundations for ensembles, orchestration languages to disruptive paradigms such as molecular and chemical computing.
