Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

This Festschrift volume, published in honor of Nissim Francez on the occasion of his 65th birthday, contains 15 papers, written by friends and colleagues, many of whom congregated at a celebratory symposium held on May 24-25, 2009, in Haifa, Israel. The theme of the symposium was Languages: From Formal to Natural, reflecting the focus of Nissim Francez' research career, which started in program verification and the semantics of programming languages and later concentrated on natural languages and computational linguistics. The papers included in this volume cover the entire spectrum of this field of research.

Mathematical Theory --- Computer Science --- Engineering & Applied Sciences --- Mathematics --- Physical Sciences & Mathematics --- Computer programming. --- Programming languages (Electronic computers) --- Computer languages --- Computer program languages --- Computer programming languages --- Machine language --- Computers --- Electronic computer programming --- Electronic data processing --- Electronic digital computers --- Programming (Electronic computers) --- Programming --- Computer science. --- Arithmetic and logic units, Computer. --- Computers. --- Computer logic. --- Mathematical logic. --- Computer Science. --- Mathematical Logic and Formal Languages. --- Mathematical Logic and Foundations. --- Logics and Meanings of Programs. --- Theory of Computation. --- Arithmetic and Logic Structures. --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Computer science logic --- Logic, Symbolic and mathematical --- Automatic computers --- Automatic data processors --- Computer hardware --- Computing machines (Computers) --- Electronic brains --- Electronic calculating-machines --- Electronic computers --- Hardware, Computer --- Computer systems --- Cybernetics --- Machine theory --- Calculators --- Cyberspace --- Arithmetic and logic units, Computer --- Computer arithmetic --- Informatics --- Science --- Circuits --- Coding theory --- Languages, Artificial --- Logic, Symbolic and mathematical. --- Logic design. --- Information theory. --- Communication theory --- Communication --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Switching theory

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Model checking technology is among the foremost applications of logic to computer science and computer engineering. The model checking community has achieved many breakthroughs, bridging the gap between theoretical computer science and hardware and software engineering, and it is reaching out to new challenging areas such as system biology and hybrid systems. Model checking is extensively used in the hardware industry and has also been applied to the verification of many types of software. Model checking has been introduced into computer science and electrical engineering curricula at universities worldwide and has become a universal tool for the analysis of systems. This Festschrift volume, published in celebration of the 25th Anniversary of Model Checking, includes a collection of 11 invited papers based on talks at the symposium "25 Years of Model Checking", 25MC, which was part of the 18th International Conference on Computer Aided Verification (CAV 2006), which in turn was part of the Federated Logic Conference (FLoC 2006) held in Seattle, WA, USA, in August 2006. Model checking is currently attracting considerable attention beyond the core technical community, and the ACM Turing Award 2007 was given in recognition of the paradigm-shifting work on this topic initiated a quarter century ago. Here we honor that achievement with the inclusion of facsimile reprints of the visionary papers on model checking by Edmund Clarke and Allen Emerson, and by Jean-Pierre Queille and Joseph Sifakis.

Mathematical logic --- Computer science --- Programming --- Computer. Automation --- programmeren (informatica) --- programmeertalen --- wiskunde --- software engineering --- logica

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

In the last few years we have all become daily users of Internet banking, social networks and cloud services. Preventing malfunctions in these services and protecting the integrity of private data from cyber attack are both current preoccupations of society at large. While modern technologies have dramatically improved the quality of software, the computer science community continues to address the problems of security by developing a theory of formal verification; a body of methodologies, algorithms and software tools for finding and eliminating bugs and security hazards. This book presents lectures delivered at the NATO Advanced Study Institute (ASI) School Marktoberdorf 2015 – ‘Verification and Synthesis of Correct and Secure Systems'. During this two-week summer school, held in Marktoberdorf, Germany, in August 2015, the lecturers provided a comprehensive view of the current state-of-the-art in a large variety of subjects, including: models and techniques for analyzing security protocols; parameterized verification; synthesis of reactive systems; software model checking; composition checking; programming by examples; verification of current software; two-player zero-sum games played on graphs; software security by information flow; equivalents – combinatorics; and analysis of synthesis with 'Big Code'. The Marktoberdorf ASIs have become a high-level scientific nucleus of the international scientific network on formal methods, and one of the major international computer science summer schools. This book will be of interest to all those seeking an overview of current theories and applications in formal verification and security.

Computer security --- Computer networks --- Software engineering --- Security measures

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

ETAPS 2007 is the tenth instance of the European Joint Conferences on Theory and Practice of Software, and thus a cause for celebration. The events that comprise ETAPS address various aspects of the system - velopment process, including speci?cation, design, implementation, analysis and improvement. The languages, methodologies and tools which support these - tivities are all well within its scope. Di?erent blends of theory and practice are represented, with an inclination towards theory with a practical motivation on the one hand and soundly based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware s- tems, and the emphasis on software is not intended to be exclusive. HistoryandPrehistoryofETAPS ETAPS as we know it is an annual federated conference that was established in 1998 by combining ?ve conferences [Compiler Construction (CC), European SymposiumonProgramming(ESOP),FundamentalApproachestoSoftware- gineering(FASE), Foundations of SoftwareScience and ComputationStructures (FOSSACS), Tools and Algorithms for Construction and Analysis of Systems (TACAS)] with satellite events.

Complex analysis --- Computer science --- Computer architecture. Operating systems --- Computer. Automation --- complexe analyse (wiskunde) --- programmeren (informatica) --- software engineering --- computernetwerken

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Computer systems --- Engineering & Applied Sciences --- Computer Science --- Verification of computer systems --- Verification. --- Verification --- 681.3*D24 --- 681.3*F22 --- 681.3*F31 --- 681.3*F22 Nonnumerical algorithms and problems: complexity of proof procedures; computations on discrete structures; geometrical problems and computations; pattern matching --See also {?681.3*E2-5}; {681.3*G2}; {?681.3*H2-3} --- Nonnumerical algorithms and problems: complexity of proof procedures; computations on discrete structures; geometrical problems and computations; pattern matching --See also {?681.3*E2-5}; {681.3*G2}; {?681.3*H2-3} --- 681.3*F31 Specifying anf verifying and reasoning about programs: assertions; invariants; mechanical verification; pre- and post-conditions (Logics and meanings of programs)--See also {681.3*D21}; {681.3*D24}; {681.3*D31}; {681.3*E1} --- Specifying anf verifying and reasoning about programs: assertions; invariants; mechanical verification; pre- and post-conditions (Logics and meanings of programs)--See also {681.3*D21}; {681.3*D24}; {681.3*D31}; {681.3*E1} --- 681.3*D24 Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- Program verification: assertion checkers; correctness proofs; reliability; validation (Software engineering)--See also {681.3*F31} --- Informatique --- Computer science --- Systèmes informatiques --- Vérification --- Artificial intelligence. Robotics. Simulation. Graphics