An operational semantics for Android activities

Etienne Payet 1 Fausto Spoto 2
1 LIM - Laboratoire d'Informatique et de Mathématiques
2 Department of Computer Science
Abstract : We define an operational semantics for a large part of the Android platform, encompassing the Dalvik bytecode but also, and more importantly, the inter-component communication mechanism used inside Android applications. This semantics is intended to provide a formal basis for the development of static analyses that consider the complex flow of information exposed by the cooperating com- ponents of Android applications.
Keywords : Dalvik Static Anal-ysis Verification Keywords Operational Semantics Theory Program analysis General Terms Languages F32 [Logics and Meanings of Programs]: Semantics of Programming Languages-Operational semantics F31 [Logics and Mean-ings of Programs]: Specifying and Verifying and Reasoning about Programs-Mechanical Verification Static Analysis Operational Semantics Android
Document type :
Conference papers
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download
https://hal.univ-reunion.fr/hal-01451693
Contributor : Réunion Univ <>
Submitted on : Friday, November 9, 2018 - 8:56:28 AM
Last modification on : Monday, September 2, 2019 - 9:42:13 AM
Long-term archiving on : Sunday, February 10, 2019 - 12:36:12 PM

File

An_operational_semantics_for_a...

Identifiers

  • HAL Id : hal-01451693, version 1

Collections

UNIV-REUNION | LIM | PAPANGUE | FST-REUNION

Citation

Etienne Payet, Fausto Spoto. An operational semantics for Android activities. ACM SIGPLAN 2014 workshop on Partial Evaluation and Program Manipulation, PEPM 2014, Jan 2014, San Diego, United States. pp.121-132. ⟨hal-01451693⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

37

Files downloads

88

Contact

CCSD