This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

Lecture Notes in Computer Science

A book, report or monograph series.

Springer's series, not a venue. A paper here belongs to some conference whose proceedings the series carried; the conference is the thing to browse by, and it sits inside this set.

Global BGP Attacks that Evade Route Monitoring

Henry Birge-Lee and others (2025) · International Conference on Passive and Active Network Measurement · Springer

History-Based Reasoning About Behavioral Subtyping

Jinting Bian and others (2024) · Theoretical Aspects of Computing · Springer

Following the Data Trail: An Analysis of IXP Dependencies

Malte Tashiro and others (2024) · International Conference on Passive and Active Network Measurement · Springer

Analysis and Formal Specification of OpenJDK's BitSet

Andy S. Tatman and others (2024) · Integrated Formal Methods · Springer

Evaluation of Parameter-Based Attacks Against Embedded Neural Networks with Laser Injection

Mathieu Dumont and others (2023) · Lecture notes in computer science · Springer Science+Business Media

Combined Fault Injection and Real-Time Side-Channel Analysis for Android Secure-Boot Bypassing

Clément Fanjas and others (2023) · Lecture notes in computer science · Springer Science+Business Media

The Effects of the Russo-Ukrainian War on Network Infrastructures Through the Lens of BGP

Zisis Tsiatsikas and others (2023) · Computer Security. ESORICS 2022 International Workshops · Springer International Publishing

Foundations for entailment checking in quantitative separation logic

Kevin Batz and others (2022) · 31st European Symposium on Programming (ESOP) · Springer

Footprint Logic for Object-Oriented Components

Frank S. de Boer and others (2022) · Formal Aspects of Component Software · Springer International Publishing

Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols

Joonwon Choi and others (2022) · Lecture notes in computer science · Springer Science+Business Media

Multi-Spot Laser Fault Injection Setup: New Possibilities for Fault Injection Attacks

Brice Colombier and others (2022) · Lecture notes in computer science · Springer Science+Business Media

Sound automation of magic wands

Thibault Dardinier and others (2022) · 34th International Conference on Computer Aided Verification (CAV) · Springer

High-Level Synthesis of Digital Circuits from Template Haskell and SDF-AP

H. H. Folmer and others (2022) · Lecture notes in computer science · Springer Science+Business Media

On Deductive Verification of an Industrial Concurrent Software Component with VerCors

Raúl E. Monti and others (2022) · Leveraging Applications of Formal Methods, Verification and Validation · Springer

Integrating ADTs in KeY and their Application to History-based Reasoning

Jinting Bian and others (2021) · 24th International Symposium on Formal Methods (FM) · Springer

SideLine: How Delay-Lines (May) Leak Secrets from Your SoC

Joseph Gravellier and others (2021) · Lecture notes in computer science · Springer Science+Business Media

What you need to know about (smart) network interface cards

Georgios P. Katsikas and others (2021) · International Conference on Passive and Active Network Measurement · Springer

Syntax-Guided Quantifier Instantiation

Aina Niemetz and others (2021) · 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems · Springer

Gobra: Modular specification and verification of Go programs

Felix A. Wolf and others (2021) · 33rd International Conference on Computer Aided Verification (CAV) · Springer

Scalable Detection of Amplification Timing Anomalies for the Superscalar TriCore Architecture

Benjamin Binder and others (2020) · Lecture notes in computer science · Springer Science+Business Media

Navigating the Universe of Z3 Theory Solvers

Nikolaj Bjørner and others (2020) · Lecture notes in computer science · Springer Science+Business Media

The 2020 expert survey on formal methods

Hubert Garavel and others (2020) · 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS) · Springer

History-Based Specification and Verification of Java Collections in KeY

Hans-Dieter A. Hiep and others (2020) · Integrated Formal Methods · Springer

A Tutorial on Verifying LinkedList Using KeY

Hans-Dieter A. Hiep and others (2020) · Deductive Software Verification: Future Perspectives · Springer International Publishing

Verifying OpenJDK's LinkedList using KeY

Hans-Dieter A. Hiep and others (2020) · Tools and Algorithms for the Construction and Analysis of Systems · Springer

State Space Reduction For Parity Automata

Christof Löding and others (2020) · 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) · Schloss Dagstuhl – Leibniz-Zentrum für Informatik

A First-Order Logic with Frames

Adithya Murali and others (2020) · 29th European Symposium on Programming (ESOP) · Springer

Witnessing Secure Compilation

Kedar S. Namjoshi and others (2020) · Lecture notes in computer science · Springer Science+Business Media

Fault Injection Characterization on Modern CPUs: From the ISA to the Micro-Architecture

Thomas Trouchkine and others (2020) · Lecture notes in computer science · Springer Science+Business Media

Alias Resolution Based on ICMP Rate Limiting

Kévin Vermeulen and others (2020) · Lecture notes in computer science · Springer Science+Business Media

Towards Formal Co-validation of Hardware and Software Timing Models of CPSs

Mihail Asăvoae and others (2019) · Lecture notes in computer science · Springer Science+Business Media

Experimental Analysis of the Laser-Induced Instruction Skip Fault Model

Jean-Max Dutertre and others (2019) · Lecture notes in computer science · Springer Science+Business Media

Reflections on Bernhard Steffen’s Physics of Software Tools

Hubert Garavel and others (2019) · Lecture notes in computer science · Springer Science+Business Media

Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction

Aman Goel and others (2019) · Lecture notes in computer science · Springer Science+Business Media

The Impact of Requirement Splitting on the Efficiency of Supervisory Control Synthesis

Martijn A. Goorden and others (2019) · Lecture notes in computer science · Springer Science+Business Media

Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools

Reiner Hähnle and others (2019) · Lecture notes in computer science · Springer Science+Business Media

Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation

Long H. Pham and others (2019) · Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings · Springer

NetSpectre: Read Arbitrary Memory over Network

Michael Schwarz and others (2019) · Lecture notes in computer science · Springer Science+Business Media

SL-COMP: Competition of Solvers for Separation Logic

Mihaela Sighireanu and others (2019) · International Conference on Tools and Algorithms for the Construction and Analysis of Systems · Springer

Verification and Evaluation of Computer and Communication Systems: 12th International Conference, VECoS 2018, Grenoble, France, September 26–28, 2018, Proceedings

Mohamed Faouzi Atig and others (2018) · Lecture notes in computer science · Springer Science+Business Media

Backwards and Forwards with Separation Logic

Callum Bannister and others (2018) · 9th International Conference on Interactive Theorem Proving (ITP) · Springer

On the Industrial Uptake of Formal Methods in the Railway Domain: A Survey with Stakeholders

Davide Basile and others (2018) · Lecture notes in computer science · Springer Science+Business Media

Continuous Formal Verification of Amazon s2n

Andrey Chudnov and others (2018) · Lecture notes in computer science · Springer Science+Business Media

The effects of adding reachability predicates in propositional separation logic

Stéphane Demri and others (2018) · 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) · Springer

The State of Fault Injection Vulnerability Detection

Thomas Given-Wilson and others (2018) · Verification and Evaluation of Computer and Communication Systems (VECoS 2018)

Btor2 , BtorMC and Boolector 3.0

Aina Niemetz and others (2018) · Lecture notes in computer science · Springer Science+Business Media

The Proof Complexity of SMT Solvers

Robert Robere and others (2018) · Lecture notes in computer science · Springer Science+Business Media

Nanofocused X-Ray Beam to Reprogram Secure Circuits

Stéphanie Anceau and others (2017) · Lecture notes in computer science · Springer Science+Business Media

The VerCors Tool Set: Verification of Parallel and Concurrent Software

Stefan Blom and others (2017) · Integrated Formal Methods · Springer

Biabduction (and Related Problems) in Array Separation Logic

James Brotherston and others (2017) · Automated Deduction – CADE 26 · Springer

Bringing order to the separation logic jungle

Qinxiang Cao and others (2017) · 15th Asian Symposium on Programming Languages and Systems (APLAS) · Springer

Non-associative Kleene Algebra and Temporal Logics

Jules Desharnais and others (2017) · Lecture notes in computer science · Springer Science+Business Media

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic

Quang Loc Le and others (2017) · Computer Aided Verification · Springer

Economy Class Crypto: Exploring Weak Cipher Usage in Avionic Communications via ACARS

Matthew Smith and others (2017) · Lecture notes in computer science · Springer Science+Business Media

Rowhammer.js: A Remote Software-Induced Fault Attack in JavaScript

Daniel Gruss and others (2016) · Lecture notes in computer science · Springer Science+Business Media

Completeness for a first-order abstract separation logic

Zhé Hóu and others (2016) · 14th Asian Symposium on Programming Languages and Systems (APLAS) · Springer

SpecCert: Specifying and Verifying Hardware-Based Security Enforcement

Thomas Letan and others (2016) · Lecture notes in computer science · Springer Science+Business Media

SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration

Jan Mrázek and others (2016) · Lecture notes in computer science · Springer Science+Business Media

Viper: A verification infrastructure for permission-based reasoning

Peter Müller and others (2016) · Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings 17 · Springer

End-to-End Verification of ARM Processors with ISA-Formal

Alastair Reid and others (2016) · Computer Aided Verification (CAV 2016)

A Decision Procedure for Separation Logic in SMT

Andrew Reynolds and others (2016) · Automated Technology for Verification and Analysis · Springer

Automatic Derivation of Platform Noninterference Properties

Oliver Schwarz and others (2016) · Lecture notes in computer science · Springer Science+Business Media

Deductive Software Verification – The KeY Book

Mattias Ulbrich and others (2016) · Springer

Debits and Credits in Petri Nets and Linear Logic

Massimo Bartoletti and others (2015) · Lecture notes in computer science · Springer Science+Business Media

Models of Circular Causality

Massimo Bartoletti and others (2015) · Lecture notes in computer science · Springer Science+Business Media

The Lean Theorem Prover (System Description)

Leonardo de Moura and others (2015) · Lecture notes in computer science · Springer Science+Business Media

A Program Construction and Verification Tool for Separation Logic

Brijesh Dongol and others (2015) · Mathematics of Program Construction · Springer

From Code Review to Fault Injection Attacks: Filling the Gap Using Fault Model Inference

Louis Dureuil and others (2015) · Lecture notes in computer science · Springer Science+Business Media

Differential Fault Intensity Analysis on PRESENT and LED Block Ciphers

Nahid Farhady Ghalaty and others (2015) · Lecture notes in computer science · Springer Science+Business Media

OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case

Stijn de Gouw and others (2015) · Computer Aided Verification · Springer

Automated Theorem Proving for Assertions in Separation Logic with All Connectives

Zhé Hóu and others (2015) · Lecture notes in computer science · Springer Science+Business Media

What You Need to Know About SDN Flow Tables

Maciej Kuźniar and others (2015) · Lecture notes in computer science · Springer Science+Business Media

A Fully Verified Container Library

Nadia Polikarpova and others (2015) · FM 2015: Formal Methods · Springer

SDN Rootkits: Subverting Network Operating Systems of Software-Defined Networks

Christian Röpke and others (2015) · Lecture notes in computer science · Springer Science+Business Media

Pyverilog: A Python-Based Hardware Design Processing Toolkit for Verilog HDL

Shinya Takamaeda-Yamazaki (2015) · Lecture notes in computer science · Springer Science+Business Media

Modular Deductive Verification of Multiprocessor Hardware Designs

Muralidaran Vijayaraghavan and others (2015) · Lecture notes in computer science · Springer Science+Business Media

Differential Cryptanalysis of Round-Reduced Simon and Speck

Farzaneh Abed and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Foundations for Decision Problems in Separation Logic with General Inductive Predicates

Timos Antonopoulos and others (2014) · Foundations of Software Science and Computation Structures · Springer

An All-in-One Toolkit for Automated White-Box Testing

Sébastien Bardin and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Using Higher-Order Contracts to Model Session Types (Extended Abstract)

Giovanni Bernardi and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Idea: Embedded Fault Injection Simulator on Smartcard

Maël Berthier and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Differential Analysis of Block Ciphers SIMON and SPECK

Alex Biryukov and others (2014) · Lecture notes in computer science · Springer Science+Business Media

The VerCors tool for verification of concurrent programs

Stefan Blom and others (2014) · International Symposium on Formal Methods · Springer

Progress as Compositional Lock-Freedom

Marco Carbone and others (2014) · Lecture notes in computer science · Springer Science+Business Media

The nuXmv Symbolic Model Checker

Roberto Cavada and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Decidable Topologies for Communicating Automata with FIFO and Bag Channels

Lorenzo Clemente and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Microcode Verification – Another Piece of the Microprocessor Verification Puzzle

Jared Davis and others (2014) · Lecture Notes in Computer Science · Springer International Publishing

Improved Differential Cryptanalysis of Round-Reduced Speck

Itai Dinur (2014) · Lecture notes in computer science · Springer Science+Business Media

Automated Code Proofs on a Formal Model of the X86

Shilpi Goel and others (2014) · Lecture notes in computer science · Springer Science+Business Media

A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors

Liana Hadarean and others (2014) · Lecture notes in computer science · Springer Science+Business Media

CBMC – C Bounded Model Checker

Daniel Kroening and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction

Suho Lee and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Communicating state transition systems for fine-grained concurrent resources

Aleksandar Nanevski and others (2014) · 23rd European Symposium on Programming Languages and Systems (ESOP) · Springer

Automating Separation Logic with Trees and Data

Ruzica Piskac and others (2014) · Computer Aided Verification · Springer

High-Level Simulation for Multiple Fault Injection Evaluation

Maxime Puys and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Combining High-Level and Low-Level Approaches to Evaluate Software Implementations Robustness Against Multiple Fault Injection Attacks

Lionel Rivière and others (2014) · Lecture notes in computer science · Springer Science+Business Media

Completeness of separation logic with inductive definitions for program verification

Makoto Tatsuta and others (2014) · International Conference on Software Engineering and Formal Methods · Springer

A Model-Based Synthesis Process for Choreography Realizability Enforcement

Marco Autili and others (2013) · Lecture notes in computer science · Springer Science+Business Media

A Theory of Agreements and Protection

Massimo Bartoletti and others (2013) · Lecture notes in computer science · Springer Science+Business Media

Formal Methods for Components and Objects, 10th International Symposium, FMCO 2011, Turin, Italy, October 3-5, 2011, Revised Selected Papers

Bernhard Beckert and others (2013) · Springer

Formally Verified System Initialisation

Andrew Boyton and others (2013) · Lecture notes in computer science · Springer Science+Business Media

Formal Verification of Hardware Synthesis

Thomas Braibant and others (2013) · Lecture notes in computer science · Springer Science+Business Media

Electromagnetic Glitch on the AES Round Counter

Amine Dehbaoui and others (2013) · Lecture notes in computer science · Springer Science+Business Media

Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types

Pierre-Malo Deniélou and others (2013) · Lecture notes in computer science · Springer Science+Business Media

dReal: An SMT Solver for Nonlinear Theories over the Reals

Sicun Gao and others (2013) · Lecture notes in computer science · Springer Science+Business Media

A Simple Separation Logic

Andreas Herzig (2013) · Logic, Language, Information, and Computation · Springer

The TAMARIN Prover for the Symbolic Analysis of Security Protocols

Simon Meier and others (2013) · Lecture notes in computer science · Springer Science+Business Media

Automating Separation Logic Using SMT

Ruzica Piskac and others (2013) · Computer Aided Verification · Springer

Charge!

Jesper Bengtson and others (2012) · Lecture notes in computer science · Springer Science+Business Media

The Security Impact of a New Cryptographic Library

Daniel J. Bernstein and others (2012) · Lecture notes in computer science · Springer Science+Business Media

Separation predicates: A taste of separation logic in first-order logic

François Bobot and others (2012) · International Conference on Formal Engineering Methods · Springer

Understanding IC3

Aaron R. Bradley (2012) · Lecture notes in computer science · Springer Science+Business Media

Model Checking and the State Explosion Problem

Edmund M. Clarke and others (2012) · Lecture notes in computer science · Springer Science+Business Media

Brief Announcement: The Degrading Effect of Forgetting on a Synchronizer

Matthias Függer and others (2012) · Lecture notes in computer science · Springer Science+Business Media

LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR

Florian Merz and others (2012) · Lecture notes in computer science · Springer Science+Business Media

LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation

Carsten Sinz and others (2012) · Lecture notes in computer science · Springer Science+Business Media

Breakthrough Silicon Scanning Discovers Backdoor in Military Chip

Sergei P. Skorobogatov and others (2012) · Lecture notes in computer science · Springer Science+Business Media

Litmus: Running Tests against Hardware

Jade Alglave and others (2011) · Lecture notes in computer science · Springer Science+Business Media

VeriSmall: Verified Smallfoot Shape Analysis

Andrew W. Appel (2011) · Lecture notes in computer science · Springer Science+Business Media

Call-by-Contract for Service Discovery, Orchestration and Recovery

Massimo Bartoletti and others (2011) · Lecture notes in computer science · Springer Science+Business Media

Combined Software and Hardware Attacks on the Java Card Control Flow

Guillaume Bouffard and others (2011) · Lecture notes in computer science · Springer Science+Business Media

Coquet: A Coq Library for Verifying Hardware

Thomas Braibant (2011) · Lecture notes in computer science · Springer Science+Business Media

BAP: A Binary Analysis Platform

David Brumley and others (2011) · Lecture notes in computer science · Springer Science+Business Media

Infer: An Automatic Program Verifier for Memory Safety of C Programs

Cristiano Calcagno and others (2011) · Lecture notes in computer science · Springer Science+Business Media

Full Reversal Routing as a Linear Dynamical System

Bernadette Charron-Bost and others (2011) · Lecture notes in computer science · Springer Science+Business Media

Towards Robustness Analysis Using PVS

Renaud Clavel and others (2011) · Lecture notes in computer science · Springer Science+Business Media

Key Exchange in IPsec Revisited: Formal Analysis of IKEv1 and IKEv2

Cas J. F. Cremers (2011) · Lecture notes in computer science · Springer Science+Business Media

VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java

Bart Jacobs and others (2011) · NASA Formal Methods · Springer

The 1st Verified Software Competition: Experience Report

Vladimir Klebanov and others (2011) · FM 2011: Formal Methods · Springer

When Clocks Fail: On Critical Paths and Clock Faults

Michel Agoyan and others (2010) · Lecture notes in computer science · Springer Science+Business Media

Fences in Weak Memory Models

Jade Alglave and others (2010) · Lecture notes in computer science · Springer Science+Business Media

Automated Verification of a Small Hypervisor

Eyad Alkassar and others (2010) · Lecture notes in computer science · Springer Science+Business Media

Design and Verification of Systems with Exogenous Coordination Using Vereofy

Christel Baier and others (2010) · Lecture notes in computer science · Springer Science+Business Media

OTAWA: An Open Toolbox for Adaptive WCET Analysis

Clément Ballabriga and others (2010) · Lecture notes in computer science · Springer Science+Business Media

Memory Leaks Detection in Java by Bi-abductive Inference

Dino Distefano and others (2010) · Lecture notes in computer science · Springer Science+Business Media

Partial, Total and General Correctness

Walter Guttmann (2010) · Lecture notes in computer science · Springer Science+Business Media

A Quick Tour of the VeriFast Program Verifier

Bart Jacobs and others (2010) · Lecture notes in computer science · Springer Science+Business Media

Cryptographic Extraction and Key Derivation: The HKDF Scheme

Hugo Krawczyk (2010) · Lecture notes in computer science · Springer Science+Business Media

A Formal Verification Study on the Rotterdam Storm Surge Barrier

Ken Madlener and others (2010) · 12th International Conference on Formal Engineering Methods (ICFEM 2010) · Springer

Abstract Object Creation in Dynamic Logic: To Be or Not to Be Created

Wolfgang Ahrendt and others (2009) · FM 2009: Formal Methods · Springer

Separating Graph Logic from MSO

Timos Antonopoulos and others (2009) · Lecture notes in computer science · Springer Science+Business Media

Beyond Shapes: Lists with Ordered Data

Kshitij Bansal and others (2009) · Lecture notes in computer science · Springer Science+Business Media

Industrial Practice in Formal Methods: A Review

Juan Carlos Bicarregui and others (2009) · Lecture notes in computer science · Springer Science+Business Media

Contract-Based Discovery and Composition of Web Services

Mario Bravetti and others (2009) · Lecture notes in computer science · Springer Science+Business Media

Future-Looking Logics on Data Words and Trees

Diego Figueira and others (2009) · Lecture notes in computer science · Springer Science+Business Media

Reasoning about Memory Layouts

Holger Gast (2009) · Lecture notes in computer science · Springer Science+Business Media

Lightweight Block Ciphers Revisited: Cryptanalysis of Reduced Round PRESENT and HIGHT

Onur Özen and others (2009) · Lecture notes in computer science · Springer Science+Business Media

Software Verification and System Assurance

John Rushby (2009) · 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods · IEEE

Completeness of Pointer Program Verification by Separation Logic

Makoto Tatsuta and others (2009) · 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods · IEEE

Contract Compliance and Choreography Conformance in the Presence of Message Queues

Mario Bravetti and others (2008) · Lecture notes in computer science · Springer Science+Business Media

A Verification Approach for System-Level Concurrent Programs

Matthias Daum and others (2008) · Lecture notes in computer science · Springer Science+Business Media

Z3: An Efficient SMT Solver

Leonardo de Moura and others (2008) · Lecture notes in computer science · Springer Science+Business Media

Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors

Dominik Dietrich and others (2008) · Lecture notes in computer science · Springer Science+Business Media

Verified Protection Model of the seL4 Microkernel

Dhammika Elkaduwe and others (2008) · Lecture notes in computer science · Springer Science+Business Media

The Beginning of Model Checking: A Personal Perspective

E. Allen Emerson (2008) · Lecture notes in computer science · Springer Science+Business Media

A Theory of Hygienic Macros

David Herman and others (2008) · 17th European Symposium on Programming (ESOP) · Springer

Enhancing Program Verification with Lemmas

Huu Hai Nguyen and others (2008) · Lecture notes in computer science · Springer Science+Business Media

A Brief Overview of PVS

Sam Owre and others (2008) · Lecture notes in computer science · Springer Science+Business Media

An Overview of Separation Logic

John Reynolds (2008) · Verified Software: Theories, Tools, Experiments · Springer

Verifying Compiler Based Refinement of Bluespec TM Specifications Using the SPIN Model Checker

Gaurav Kumar Singh and others (2008) · Lecture notes in computer science · Springer Science+Business Media

Verified Process-Context Switch for C-Programmed Kernels

Artem Starostin and others (2008) · Lecture notes in computer science · Springer Science+Business Media

Scalable Shape Analysis for Systems Code

Hongseok Yang and others (2008) · Lecture notes in computer science · Springer Science+Business Media

Cooperative Repositories for Formal Proofs

Pierre Corbineau and others (2007) · Lecture notes in computer science · Springer Science+Business Media

An Introduction to Context Logic

Philippa Anne Gardner and others (2007) · Lecture notes in computer science · Springer Science+Business Media

On the Complexity of Reasoning About Dynamic Policies

Stefan Göller (2007) · Lecture notes in computer science · Springer Science+Business Media

Fault Attacks for CRT Based RSA: New Attacks, New Results, and New Countermeasures

Chong Hee Kim and others (2007) · Lecture notes in computer science · Springer Science+Business Media

On Synthesizing Controllers from Bounded-Response Properties

Oded Maler and others (2007) · Lecture notes in computer science · Springer Science+Business Media

Test Coverage for Continuous and Hybrid Systems

Tarik Nahhal and others (2007) · Lecture notes in computer science · Springer Science+Business Media

Using XCAP to Certify Realistic Systems Code: Machine Context Management

Zhaozhong Ni and others (2007) · Lecture notes in computer science · Springer Science+Business Media

Information Hiding in Software with Mixed Boolean-Arithmetic Transforms

Yongxin Zhou and others (2007) · Lecture notes in computer science · Springer Science+Business Media

Predicting Secret Keys Via Branch Prediction

Onur Acıiçmez and others (2006) · Lecture notes in computer science · Springer Science+Business Media

A Content Based Mathematical Search Engine: Whelp

Andrea Asperti and others (2006) · Lecture notes in computer science · Springer Science+Business Media

Boogie: A Modular Reusable Verifier for Object-Oriented Programs

Mike Barnett and others (2006) · Lecture notes in computer science · Springer Science+Business Media

Improving SHA-2 Hardware Implementations

Ricardo Chaves and others (2006) · Lecture notes in computer science · Springer Science+Business Media

A Local Shape Analysis Based on Separation Logic

Dino Distefano and others (2006) · Tools and Algorithms for the Construction and Analysis of Systems · Springer

Towards Self-verification of HOL Light

John Harrison (2006) · Lecture notes in computer science · Springer Science+Business Media

Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions

Ioannis T. Kassios (2006) · FM 2006: Formal Methods · Springer

Hoare logic in the abstract

Ursula Martin and others (2006) · 20th International Workshop on Computer Science Logic (CSL) · Springer

Lazy Abstraction with Interpolants

Kenneth L. McMillan (2006) · Lecture notes in computer science · Springer Science+Business Media

Separation logic for higher-order store

Bernhard Reus and others (2006) · 20th International Workshop on Computer Science Logic (CSL) · Springer

Optically Enhanced Position-Locked Power Analysis

Sergei P. Skorobogatov (2006) · Lecture notes in computer science · Springer Science+Business Media

Symbolic Execution with Separation Logic

Josh Berdine and others (2005) · Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings · Springer

BI Hyperdoctrines and Higher-Order Separation Logic

Bodil Biering and others (2005) · Lecture notes in computer science · Springer Science+Business Media

From separation logic to first-order logic

Cristiano Calcagno and others (2005) · 8th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS) · Springer

On the Verification of Memory Management Mechanisms

Iakov Dalinger and others (2005) · Lecture notes in computer science · Springer Science+Business Media

On the Correctness of Operating System Kernels

Mauro Gargano and others (2005) · Lecture notes in computer science · Springer Science+Business Media

DFA on AES

Christophe Giraud (2005) · Lecture notes in computer science · Springer Science+Business Media

A HOL Theory of Euclidean Space

John Harrison (2005) · Lecture notes in computer science · Springer Science+Business Media

Clause Form Conversions for Boolean Circuits

Paul B. Jackson and others (2005) · Lecture notes in computer science · Springer Science+Business Media

Real Time Temporal Logic: Past, Present, Future

Oded Maler and others (2005) · Lecture notes in computer science · Springer Science+Business Media

Optimizing SHA-1 Hash Function for High Throughput with a Partial Unrolling Study

Harris E. Michail and others (2005) · Lecture notes in computer science · Springer Science+Business Media

A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic

Tom Ridge and others (2005) · Theorem Proving in Higher Order Logics · Springer

Mining Temporal Specifications for Error Detection

Westley R. Weimer and others (2005) · Lecture notes in computer science · Springer Science+Business Media

A Decidable Fragment of Separation Logic

Josh Berdine and others (2004) · FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science · Springer

Correlation Power Analysis with a Leakage Model

Éric Brier and others (2004) · Lecture notes in computer science · Springer Science+Business Media

C-CoRN, the Constructive Coq Repository at Nijmegen

Luı́s Cruz-Filipe and others (2004) · Lecture notes in computer science · Springer Science+Business Media

Who is Pointing When to Whom?

Dino Distefano and others (2004) · Lecture notes in computer science · Springer Science+Business Media

On Timed Automata with Input-Determined Guards

Deepak D’Souza and others (2004) · Lecture notes in computer science · Springer Science+Business Media

The Boundary Between Decidability and Undecidability for Transitive-Closure Logics

Neil Immerman and others (2004) · Lecture notes in computer science · Springer Science+Business Media

Generalized Records and Spatial Conjunction in Role Logic

Viktor Kuncak and others (2004) · Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings · Springer

Are User Runtime Estimates Inherently Inaccurate?

Cynthia Bailey Lee and others (2004) · Lecture notes in computer science · Springer Science+Business Media

On Recognizable Timed Languages

Oded Maler and others (2004) · Lecture notes in computer science · Springer Science+Business Media

Why Model Checking Can Improve WCET Analysis

Alexander Metzner (2004) · Lecture notes in computer science · Springer Science+Business Media

Reasoning about Dynamic Policies

Riccardo Pucella and others (2004) · Lecture notes in computer science · Springer Science+Business Media

Extending Separation Logic with Fixpoints and Postponed Substitution

Élodie-Jane Sims (2004) · Algebraic Methodology and Software Technology · Springer

Towards mechanized program verification with separation logic

Tjark Weber (2004) · 18th International Workshop on Computer Science Logic (CSL) · Springer

Formal Proof Sketches

Freek Wiedijk (2004) · Lecture notes in computer science · Springer Science+Business Media

Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone

Reinhard Wilhelm (2004) · Lecture notes in computer science · Springer Science+Business Media

The EM Side—Channel(s)

Dakshi Agrawal and others (2003) · Lecture notes in computer science · Springer Science+Business Media

Formal Methods at the Crossroads. From Panacea to Foundational Support

Bernhard K. Aichernig and others (2003) · Lecture notes in computer science · Springer Science+Business Media

Differential Fault Analysis on A.E.S

Pierre Dusart and others (2003) · Lecture notes in computer science · Springer Science+Business Media

Formal Specification and Verification of ARM6

Anthony C. J. Fox (2003) · Lecture notes in computer science · Springer Science+Business Media

A New Extraction for Coq

Pierre Letouzey (2003) · Lecture notes in computer science · Springer Science+Business Media

A Simple Power-Analysis (SPA) Attack on Implementations of the AES Key Expansion

Stefan Mangard (2003) · Lecture notes in computer science · Springer Science+Business Media

Proving Pointer Programs in Higher-Order Logic

Farhad Mehta and others (2003) · Lecture notes in computer science · Springer Science+Business Media

A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts

Cees Pierik and others (2003) · Formal Methods for Open Object-Based Distributed Systems · Springer

A Differential Fault Attack Technique against SPN Structures, with Application to the AES and Khazad

Gilles Piret and others (2003) · Lecture notes in computer science · Springer Science+Business Media

Processor Pipelines and Their Properties for Static WCET Analysis

Jakob Engblom and others (2002) · Lecture notes in computer science · Springer Science+Business Media

Synthesizing Monitors for Safety Properties

Klaus Havelund and others (2002) · Lecture notes in computer science · Springer Science+Business Media

An FPGA Based SHA-256 Processor

Kurt K. Ting and others (2002) · Lecture notes in computer science · Springer Science+Business Media

Fault Diagnosis for Timed Automata

Stavros Tripakis (2002) · Lecture notes in computer science · Springer Science+Business Media

A Semantic Basis for Local Reasoning

Hongseok Yang and others (2002) · Foundations of Software Science and Computation Structures · Springer

Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS

Andrew A. Adams and others (2001) · Lecture notes in computer science · Springer Science+Business Media

On the (Im)possibility of Obfuscating Programs

Boaz Barak and others (2001) · Lecture notes in computer science · Springer Science+Business Media

Formal Verification of the VAMP Floating Point Unit

Christoph Berg and others (2001) · Lecture notes in computer science · Springer Science+Business Media

Computability and Complexity Results for a Spatial Assertion Language for Data Structures

Cristiano Calcagno and others (2001) · Foundations of Software Technology and Theoretical Computer Science (FSTTCS) · Springer

Microarchitecture Verification by Compositional Model Checking

Ranjit Jhala and others (2001) · Lecture notes in computer science · Springer Science+Business Media

On Bounded Specifications

Orna Kupferman and others (2001) · Lecture notes in computer science · Springer Science+Business Media

Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques

Steve McKeever and others (2001) · Lecture notes in computer science · Springer Science+Business Media

Hardware Synthesis Using SAFL and Application to Processor Design

Alan Mycroft and others (2001) · Lecture notes in computer science · Springer Science+Business Media

Local Reasoning about Programs that Alter Data Structures

Peter W. O'Hearn and others (2001) · Computer Science Logic · Springer

ElectroMagnetic Analysis (EMA): Measures and Counter-measures for Smart Cards

Jean-Jacques Quisquater and others (2001) · Lecture notes in computer science · Springer Science+Business Media

A Language-Based Approach to Security

Fred B. Schneider and others (2001) · Lecture notes in computer science · Springer Science+Business Media

Soft Scheduling for Hardware

Richard R. Sharp and others (2001) · Lecture notes in computer science · Springer Science+Business Media

Verifying Advanced Microarchitectures that Support Speculation and Exceptions

Ravi Mohan Hosabettu and others (2000) · Lecture notes in computer science · Springer Science+Business Media

Timed Automata

Rajeev Alur (1999) · Lecture notes in computer science · Springer Science+Business Media

Symbolic Model Checking without BDDs

Armin Biere and others (1999) · Tools and Algorithms for the Construction and Analysis of Systems (TACAS) · Springer Science+Business Media

A WP-calculus for OO

Frank S. de Boer (1999) · Foundations of Software Science and Computation Structures · Springer

A Machine-Checked Theory of Floating Point Arithmetic

John Harrison (1999) · Lecture notes in computer science · Springer Science+Business Media

Language-Based Security

Dexter C. Kozen (1999) · Lecture notes in computer science · Springer Science+Business Media

An Overview of Hybrid Simulation Phenomena and Their Support by Simulation Packages

Pieter J. Mosterman (1999) · Lecture notes in computer science · Springer Science+Business Media

On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems

Stavros Tripakis and others (1999) · Lecture notes in computer science · Springer Science+Business Media

Model Checking TLA+ Specifications

Yuan Yu and others (1999) · Lecture notes in computer science · Springer Science+Business Media

A Lightweight Approach to Formal Methods

Sten Agerholm and others (1998) · Applied Formal Methods — FM-Trends 98 · Springer

Slack elasticity in concurrent computing

Rajit Manohar and others (1998) · Lecture notes in computer science · Springer Science+Business Media

Verification of an implementation of Tomasulo's algorithm by compositional model checking

Kenneth L. McMillan (1998) · Lecture notes in computer science · Springer Science+Business Media

Processor verification with precise exceptions and speculative execution

Jun Sawada and others (1998) · Lecture notes in computer science · Springer Science+Business Media

A logic of object-oriented programs

Martín Abadi and others (1997) · TAPSOFT '97: Theory and Practice of Software Development · Springer

Differential fault analysis of secret key cryptosystems

Eli Biham and others (1997) · Lecture notes in computer science · Springer Science+Business Media

On the Importance of Checking Cryptographic Protocols for Faults

Dan Boneh and others (1997) · Lecture notes in computer science · Springer Science+Business Media

Using reflection to build efficient and certified decision procedures

Samuel Boutin (1997) · Lecture notes in computer science · Springer Science+Business Media

Mechanizing verification of arithmetic circuits: SRT division

Deepak Kapur and others (1997) · Lecture notes in computer science · Springer Science+Business Media

State clock logic: A decidable real-time logic

Jean-François Raskin and others (1997) · Lecture notes in computer science · Springer Science+Business Media

Alternating automata: Unifying truth and validity checking for temporal logics

Moshe Y. Vardi (1997) · Lecture notes in computer science · Springer Science+Business Media

The embedded software of an electricity meter: An experience in using formal methods in an industrial project

André Arnold and others (1996) · Lecture notes in computer science · Springer Science+Business Media

STeP: Deductive-algorithmic verification of reactive and real-time systems

Nikolaj Bjørner and others (1996) · Lecture notes in computer science · Springer Science+Business Media

ACL2 theorems about commercial microprocessors

Bishop C. Brock and others (1996) · Lecture notes in computer science · Springer Science+Business Media

Experiments in automating hardware verification using inductive proof planning

Francisco J. Cantú-Ortiz and others (1996) · Lecture notes in computer science · Springer Science+Business Media

Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem

Patrice Godefroid (1996) · Lecture notes in computer science · Springer Science+Business Media

A mizar mode for HOL

John Harrison (1996) · Lecture notes in computer science · Springer Science+Business Media

Experiments in theorem proving and model checking for protocol verification

Klaus Havelund and others (1996) · Lecture notes in computer science · Springer Science+Business Media

Mechanically verifying a family of multiplier circuits

Deepak Kapur and others (1996) · Computer Aided Verification (CAV) · Springer Berlin Heidelberg

Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems

Paul C. Kocher (1996) · Advances in Cryptology — CRYPTO '96 · Springer Berlin Heidelberg

Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR

Gavin Lowe (1996) · Tools and Algorithms for the Construction and Analysis of Systems · Springer

Automated deduction and formal methods

John Rushby (1996) · Lecture notes in computer science · Springer Science+Business Media

The METAFrame'95 environment

Bernhard Steffen and others (1996) · Lecture notes in computer science · Springer Science+Business Media

A mixed linear and non-linear logic: Proofs, terms and models

P. N. Benton (1995) · Lecture notes in computer science · Springer Science+Business Media

Quantitative evaluation of formal based synthesis in ASIC design

G. Bezzi and others (1995) · Lecture notes in computer science · Springer Science+Business Media

Formal methods technology transfer: Impediments and innovation (abstract)

Dan Craigen (1995) · Lecture notes in computer science · Springer Science+Business Media

An automata theory dedicated towards formal circuit synthesis

Dirk Eisenbiegler and others (1995) · Lecture notes in computer science · Springer Science+Business Media

The CMU master of Software Engineering core curriculum

David Garlan and others (1995) · Lecture notes in computer science · Springer Science+Business Media

Automatic datapath abstraction in hardware systems

Ramin Hojati and others (1995) · Lecture notes in computer science · Springer Science+Business Media

A formal framework for high level synthesis

Thomas Kröpf and others (1995) · Lecture notes in computer science · Springer Science+Business Media

A tutorial on using PVS for hardware verification

Sam Owre and others (1995) · Lecture notes in computer science · Springer Science+Business Media

Anatomy of the Pentium bug

Vaughan Pratt (1995) · Lecture notes in computer science · Springer Science+Business Media

An integration of model checking with automated proof checking

Sreeranga P. Rajan and others (1995) · Lecture notes in computer science · Springer Science+Business Media

Alternating automata and program verification

Moshe Y. Vardi (1995) · Lecture notes in computer science · Springer Science+Business Media

Automatic verification of pipelined microprocessor control

Jerry R. Burch and others (1994) · Computer Aided Verification (CAV) · Springer

Automatic verification of finite-state concurrent systems

Edmund M. Clarke (1994) · Lecture notes in computer science · Springer Science+Business Media

Formalising British rail's signalling rules

Trevor King (1994) · Lecture notes in computer science · Springer Science+Business Media

An engineering approach to formal digital system design

Mats A. Larsson (1994) · Lecture notes in computer science · Springer Science+Business Media

The Alf proof editor and its proof engine

Lena Magnusson and others (1994) · Lecture notes in computer science · Springer Science+Business Media

A tool for symbolic program verification and abstraction

Susanne Graf and others (1993) · Lecture notes in computer science · Springer Science+Business Media

BDD-Based debugging of designs using language containment and fair CTL

Ramin Hojati and others (1993) · Lecture notes in computer science · Springer Science+Business Media

Verification of a multiplier: 64 bits and beyond

Robert P. Kurshan and others (1993) · Lecture notes in computer science · Springer Science+Business Media

Increasing the versatility of heuristic based theorem provers

Alistair Manning and others (1993) · Lecture notes in computer science · Springer Science+Business Media

Partial-order methods for temporal verification

Pierre Wolper and others (1993) · Lecture notes in computer science · Springer Science+Business Media

Logics and models of real time: A survey

Rajeev Alur and others (1992) · Lecture notes in computer science · Springer Science+Business Media

From timed to hybrid systems

Oded Maler and others (1992) · Lecture notes in computer science · Springer Science+Business Media

PVS: A prototype verification system

Sam Owre and others (1992) · Lecture notes in computer science · Springer Science+Business Media

The use of proof plans to sum series

Toby Walsh and others (1992) · Lecture notes in computer science · Springer Science+Business Media

An overview of HP-SL

Stephen Bear (1991) · Lecture notes in computer science · Springer Science+Business Media

Model checking and modular verification

Orna Grümberg and others (1991) · Lecture notes in computer science · Springer Science+Business Media

Verification of synchronous circuits by symbolic logic simulation

Randal E. Bryant (1990) · Lecture Notes in Computer Science · Springer New York

Verification of synchronous sequential machines based on symbolic execution

Olivier Coudert and others (1990) · Lecture notes in computer science · Springer Science+Business Media

The complexity of graph problems for succinctly represented graphs

Antonio Lozano and others (1990) · Lecture notes in computer science · Springer Science+Business Media

Realizable and unrealizable specifications of reactive systems

Martı́n Abadi and others (1989) · Lecture notes in computer science · Springer Science+Business Media

A synthesis of two approaches for verifying finite state concurrent systems

E. M. Clarke and others (1989) · Lecture notes in computer science · Springer Science+Business Media

Timing assumptions and verification of finite-state concurrent systems

David L. Dill (1989) · Lecture notes in computer science · Springer Science+Business Media

Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions draft

Robert W. Harper and others (1989) · Lecture notes in computer science · Springer Science+Business Media

Semantics of Digital Circuits

Carlos Delgado Kloos (1987) · Lecture notes in computer science · Springer Science+Business Media

Purely functional implementation of a logic

F.K. Hanna and others (1986) · Lecture notes in computer science · Springer Science+Business Media

The glory of the past

Orna Lichtenstein and others (1985) · Lecture notes in computer science · Springer Science+Business Media

On expressive interpretations of a Hoare-logic for Clarke's language L4

Bernhard Josko (1984) · Lecture notes in computer science · Springer Science+Business Media

Specification and verification of concurrent systems in CESAR

J. P. Queille and others (1982) · 5th International Symposium on Programming · Springer

The algebra of functional programs: Function level reasoning, linear equations, and extended definitions

John Backus (1981) · Lecture notes in computer science · Springer Science+Business Media

Design and synthesis of synchronization skeletons using branching time temporal logic

Edmund M. Clarke and others (1981) · Logic of Programs · Springer

Impartiality, justice and fairness: The ethics of concurrent termination

Daniel J. Lehmann and others (1981) · Lecture notes in computer science · Springer Science+Business Media

First-Order Dynamic Logic

David Harel (1979) · Springer

Lcf: A way of doing proofs with a machine

Robin Milner (1979) · Lecture notes in computer science · Springer Science+Business Media

Exercises in denotational semantics

Krzysztof R. Apt and others (1976) · Lecture notes in computer science · Springer Science+Business Media

Compiler generation using denotational semantics

Peter D. Mosses (1976) · Lecture notes in computer science · Springer Science+Business Media

Towards a theory of type structure

John C. Reynolds (1974) · Programming Symposium · Springer

Lecture Notes in Computer Science

Inside this

313 references