Practical API Protocol Checking with Access Permissions

No abstract is available for this paper.

• Publication year

  2009

• Venue

  European Conference on Object-Oriented Programming

• Publication date

  2009-07-30

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/978-3-642-03013-0_10
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Behavioral Specifications of Businesses and Systems

  2012cited by this paper
• Resource Usage Protocols for Iterators

  2009cited by this paper
• Api protocol compliance in object-oriented software

  2009cited by this paper
• Verifying correct usage of atomic blocks and typestate

  2008cited by this paper
• PLURAL: checking protocol compliance under aliasing

  2008cited by this paper
• Finding programming errors earlier by evaluating runtime monitors ahead-of-time

  2008influential reference
• Permissions to Specify the Composite Design Pattern

  2008cited by this paper
• Separation logic, abstraction and inheritance

  2008cited by this paper
• Adaptive Online Program Analysis

  2007cited by this paper
• ACSAR: Software Model Checking with Transfinite Refinement

  2007cited by this paper
• Modular typestate checking of aliased objects

  2007cited by this paper
• ECOOP 2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30 - August 3, 2007, Proceedings

  2007cited by this paper
• Tracking Linear and Affine Resources with Java(X)

  2007cited by this paper
• Iterator specification with typestates

  2006cited by this paper
• Effective typestate verification in the presence of aliasing

  2006influential reference
• Reasoning about iterators with separation logic

  2006cited by this paper
• Lightweight object specification with typestates

  2005cited by this paper
• Verifying safety policies with size properties and alias controls

  2005cited by this paper
• Connecting effects and uniqueness with adoption

  2005cited by this paper
• Deriving object typestates in the presence of inter-object references

  2005cited by this paper
• DynaMine: finding common error patterns by mining software revision histories

  2005cited by this paper
• ECOOP 2004 – Object-Oriented Programming

  2004cited by this paper
• Typestates for Objects

  2004influential reference
• The fugue protocol checker: is your software baroque? technical report msr-tr-2004-07

  2004influential reference
• Checking Interference with Fractional Permissions

  2003cited by this paper
• An effective theory of type refinements

  2003cited by this paper
• Verification of Object-Oriented Programs with Invariants

  2003influential reference
• Resource usage analysis

  2002cited by this paper
• Lazy abstraction

  2002cited by this paper
• Flow-sensitive type qualifiers

  2002cited by this paper
• Enforcing high-level protocols in low-level software

  2001influential reference
• Automatically validating temporal safety properties of interfaces

  2001cited by this paper
• JML: A Notation for Detailed Design

  1999influential reference
• Linear Types can Change the World!

  1990cited by this paper
• Statecharts: A Visual Formalism for Complex Systems

  1987cited by this paper
• Typestate: A programming language concept for enhancing software reliability

  1986cited by this paper
• Verification

  1917influential reference
• Ieee Transactions on Software Engineering 1 Modular Pluggable Analyses for Data Structure Consistency

  year unknowncited by this paper

• Law and Order for Typestate with Borrowing

  2024cites this paper
• Building a Framework to Improve the User Experience of Static Analysis Tools

  2024cites this paper
• Clog: A Declarative Language for C Static Code Checkers

  2024cites this paper
• Coconut: Typestates for C++

  2022cites this paper
• FUM - A Framework for API Usage constraint and Misuse Classification

  2022influential citation
• Accumulation Analysis

  2022cites this paper
• Theorems for free from separation logic specifications

  2021cites this paper
• Typechecking Java Protocols with [St]Mungo

  2020cites this paper
• A survey on the use of access permission-based specifications for program verification

  2020cites this paper
• Formal Techniques for Distributed Objects, Components, and Systems: 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings

  2020cites this paper
• Behavioural Separation with Parallel Usages for a Core Object-Oriented Language

  2020cites this paper
• Verifying correct usage of context-free API protocols

  2020cites this paper
• Towards Generating Thread-Safe Classes Automatically

  2020influential citation
• A reduction semantics for direct-style asynchronous observables

  2019cites this paper
• Revisiting memory assignment semantics in imperative programming languages

  2019cites this paper
• Automatic Inference of Symbolic Permissions for Single-threaded Java Programs

  2019cites this paper
• Access Permission-based Program Verification: A survey

  2019influential citation
• Decidable subtyping for path dependent types

  2019cites this paper
• Obsidian

  2019cites this paper
• Automatic Inference of Symbolic Permissions for Sequential Java Programs

  2019cites this paper
• Sip4J: Statically inferring permission-based specifications for sequential Java programs

  2019cites this paper
• Checking JML-encoded finite state machine properties

  2018cites this paper
• 14 Mungo and StMungo: Tools for Typechecking Protocols in Java

  2017cites this paper
• Typechecking protocols with Mungo and StMungo: A session type toolchain for Java

  2017cites this paper
• Trace Properties from Separation Logic Specifications

  2017cites this paper
• Presburger-Definable Parameterized Typestates

  2017cites this paper
• Typechecking protocols with Mungo and StMungo

  2016cites this paper
• 15 : 2 Program Tailoring : Slicing by Sequential Criteria

  2016cites this paper
• Developing usable APIs with XP and cognitive dimensions

  2016cites this paper
• Program Tailoring: Slicing by Sequential Criteria

  2016cites this paper
• The Design and Formalization of Mezzo, a Permission-Based Programming Language

  2016cites this paper
• Behaviour abstraction adequacy criteria for API call protocol testing

  2016cites this paper
• Rely-guarantee protocols for safe interference over shared memory

  2015cites this paper
• Searching the State Space: A Qualitative Study of API Protocol Usability

  2015cites this paper
• Objects as session-typed processes

  2015cites this paper
• Usability Hypotheses in the Design of Plaid

  2014cites this paper
• Structuring Documentation to Support State Search: A Laboratory Experiment about Protocol Programming

  2014cites this paper
• The extent of empirical evidence that could inform evidence-based design of programming languages : a systematic mapping study

  2014cites this paper
• Foundations of Typestate-Oriented Programming

  2014influential citation
• Algorithmic verification of procedural programs in the presence of code variability

  2014cites this paper
• Theoretical and practical aspects of typestate

  2014cites this paper
• Model-Checking Higher-Order Programs with Recursive Types

  2013cites this paper
• Programming with permissions in Mezzo

  2013cites this paper
• Inlined Reference Monitors : Certification,Concurrency and Tree Based Monitoring

  2013cites this paper
• Behaviour Abstraction Coverage as Black-Box Adequacy Criteria

  2013cites this paper
• Automatic conformance checking for migrating software systems to cloud infrastructures and platforms

  2013cites this paper
• A Retrospective on Aliasing Type Systems: 2012-2022

  2013cites this paper
• Protocol programmability

  2013influential citation
• TreeDroid: a tree automaton based approach to enforcing data processing policies

  2012influential citation
• Impact analysis for distributed event-based systems

  2012cites this paper
• A type system for borrowing permissions

  2012cites this paper
• Automated Verification of Specifications with Typestates and Access Permissions

  2012cites this paper
• An introduction to Mezzo

  2012cites this paper
• Modular Session Types for Objects

  2012cites this paper
• Predictive and Programmable Testing of Concurrent and Cloud Systems

  2012cites this paper
• A Type System for Borrowing Permissions (CMU-CS-11-142)

  2012cites this paper
• Probabilistic, modular and scalable inference of typestate specifications

  2011cites this paper
• Automated program verification made SYMPLAR: symbolic permissions for lightweight automated reasoning

  2011cites this paper
• An Empirical Study of Object Protocols in the Wild

  2011cites this paper
• Gradual Typestate

  2011cites this paper
• TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs

  2011cites this paper
• The Logical Verification of Security Protocols

  2011cites this paper
• Exploiting program and property structure for efficient runtime monitoring

  2011influential citation
• CREATING APPLICATION PROGRAMMING INTERFACE CODE TEMPLATES FROM USAGE PATTERNS

  2011cites this paper
• Lightweight Verification of a Multi-Task Threaded Server: A Case Study With The Plural Tool

  2011cites this paper
• Checking Concurrent Typestate with Access Permissions in Plural: A Retrospective

  2011cites this paper
• What should developers be aware of? An empirical study on the directives of API documentation

  2011cites this paper
• The “ Who ’ s Yo Daddy ? ” Problem Or : Solvin ’ Concurren ’ Axcess Issues wit Computers

  2011cites this paper
• Abstraction for model checking robot behaviour

  2011cites this paper
• Impact analysis for event-based components and systems

  2010cites this paper
• Polymorphic Access Permissions

  2010cites this paper
• API Conformance Verification for Java Programs

  2010cites this paper
• Types for Correct Concurrent API Usage

  2010influential citation
• Fraction Polymorphic Permission Inference

  2010cites this paper
• A theory of typestate-oriented programming

  2010cites this paper
• Polymorphic Fractional Permission Inference

  2010cites this paper
• Modular session types for distributed object-oriented programming

  2010cites this paper
• Towards a typed 3-address IR from ICode (inspired in Soot’s Jimple)

  2010cites this paper
• Helios: impact analysis for event-based components and systems

  2010cites this paper
• DynXML: safely programming the dynamic web

  2010cites this paper
• Frameworks on the Rise

  2009cites this paper
• Api protocol compliance in object-oriented software

  2009cites this paper
• Typestate protocol specification in JML

  2009cites this paper
• Proving Programs Correct Using Plain Old Java Types

  2009cites this paper
• Typestate-oriented programming

  2009cites this paper
• Helios : Impact Analysis for Event-Based Systems

  2009cites this paper