PUBLICATIONS

PUBLICATIONS

This page contains an exhaustive list of scientific publications that present the architecture and the main components of JuliaSoft. In particular [SPO16] presents the overall structure of the Julia analyzer of Java, and [BFS17] summarizes Julia’s results on OWASP benchmarks.
Many other papers present single checkers or analyses performed by Julia. For instance, [ELMSS15] formalized the injection checker, [Spot11] introduced the main components of the nullness and basic nullness checkers, while [SMP10] presented Julia’s termination analysis.

2018

[SFS18] R. Salvia, P. Ferrara, F. Spoto and A. Cortesi: “Static Detection of Leaks across Intents” Trustcom 2018
[FOS18] P. Ferrara, L. Olivieri and F.Spoto: “Tailoring Taint Analysis to GDPR” APF 2018
[FCS18] P. Ferrara, A. Cortesi and F. Spoto: “CIL to Java-bytecode Translation for Static Analysis Leveraging” FormaliSE 2018. ACM SIGSOFT Distinguished Paper Award
[MCF18] A. Mandal, A. Cortesi, P. Ferrara, F. Panarotto and F. Spoto: “Vulnerability Analysis of Android Auto Infotainment Apps” CF 2018
[FS18] Pietro Ferrara, Fausto Spoto: “Static Analysis for GDPR Compliance” ITASEC2018

2017

[BFS17] Elisa Burato , Pietro Ferrara, and Fausto Spoto  “Security Analysis of the OWASP Benchmark with Julia”  ITA-SEC 2017

2016

[SPO16] Fausto Spoto  “The Julia Static Analyzer for Java”  SAS 2016
[ELMST16] Michael D. Ernst, Alberto Lovato, Damiano Macedonio, Fausto Spoto, Javier Thaine  “Locking discipline inference and checking”  ICSE 2016: 1133-1144
[EMMS16] Michael D. Ernst, Damiano Macedonio, Massimo Merro, Fausto Spoto  “Semantics for Locking Specifications” NFM 2016: 355-372

2015

[ELMSS15] Michael D.Ernst,  Alberto Lovato, Damiano Macedonio, Ciprian Spiridon, Fausto Spoto  “Boolean Formulas for the Static Identification of Injection Attacks in Java” LPAR2015: 130-14 5
[EMMS15] Michael D.Ernst, Damiano  Macedonio ,Massimo Merro, Fausto Spoto “Semantics for Locking Specifications”  CoRR abs/1501.05338 (2015 )

2014

[PMS14] Étiyenne Payet, Fred Mesnard, Fausto Spoto “Non-Termination Analysis of Java Bytecode” CoRR abs/1401.5292 (2014 )
[SS14] Enrico Scapin, Fausto Spoto “Field-Sensitive unreachability and non-cyclicity analysis” Sci Comput. Program” 95: 359-375 (2015 )
[PS14] Étienne Payet, Fausto Spoto “An operational semantics for android activities” PEPM 2014 121-132
[LMS14] Alberto Lovato, Damiano Macedonio, Fausto Spoto “A Thread-Safe Library for Binary Decision Diagrams” SEFM 2014: 35-4 9

2013

[NS13] Durica Nikolic, Fausto Spoto “Inferring complete initialization of arrays” Theor. Comput. Sci. 484: 16-40
[NS13a]Durica Nikolic, Fausto Spoto “Reachability analysis of program variables” ACM Trans. Program. Lang.  Syst. 35(4): 14

2012

[PS12] Étienne Payet, Fausto Spoto “Static analysis of Android programs” Information & Software Technology 54(11): 1192-1201 (2012 )
[NS12b] Durica Nikolic, Fausto Spoto “Reachability Analysis of Program Variables” IJCAR 2012: 423-43 8
[NS12a] Durica Nikolic, Fausto Spoto “Definite Expression Aliasing Analysis for Java Bytecode”  ICTAC 2012: 74-8 9
[NS12] Durica Nikolic, Fausto Spoto “Automaton-Based Array Initialization Analysis”  LATA 2012: 420-432

2011

[Spot11]  Fausto Spoto  “Precise null-pointer analysis” Software and System Modeling 10(2): 219-252
[PS11] Étienne Payet, Fausto Spoto  “Static Analysis of Android Programs” CADE 2011: 439-445
[SE11] Fausto Spoto, Michel D. Ernest  “Inference of field initialization” ICSE 2011: 231-240

2010

[SE10]  Fausto Spoto, Étienne Payet  “Magic-sets for localised analysis of Java bytecode” Higher-Order an Symbolic Computation 23(1): 29-8 6
[SMP10]  Fausto Spoto, Fred Mesnard, Étienne Payet “A termination analyzer for Java bytecode based on path-length” ACM Trans. Program  Lang.Syst. 32(3)
[Spot10] Fausto Spoto “The Nullness Analyser of Julia ” LPAR (Dakar) (2010) 405-424

2009

[PS09] Étienne Payet, Fausto Spoto ” Experiments with Non-Termination Analysis for Java Bytecode” Electr. Notes Theor.  Comput. Sci. 253(5): 83-96
[SLM09] Fausto Spoto, Lunjin Lu, Fred Mesnard “Using CLP Simplifications to Improve Java Bytecode Termination Analysis” Electr. Notes. Theor. Comput. Sci. 253(5): 129-144

2008

[Spot08] Fausto Spoto “Nullness Analysis in Boolean Form” SEFM 2008: 21-30

2007

[Spot07] Fausto Spoto “Optimality and condensing of information flow through linear refinement” Theor. Comput. Sci. 388(1-3): 53-82 (2007)
[PS07] Étienne Payet, Fausto Spoto “Magic-Sets Transformation for the Analysis of Java Bytecode”  SAS 2007: 452-46  7

2006

[HS06a] Patricia M. Hill, Fausto Spoto “Deriving escape analysis by abstract interpretation”  Higher-Order and Symbolic Computation 19(4): 415-463 (2006)
[RS06] Stefano Rossignoli, Fausto Spoto “Detecting Non-cyclicity by Abstract Compilation into Boolean Functions”  VMCAI 2006: 95-110
[HS06] Patricia M.Hill, Fausto Spoto “Deriving Escape Analysis by Abstract Interpretation: Proofs of results   CoRR abs/cs/0607101 (2006)

2005

[Spot05] Fausto Spoto “Information Flow Is Linear Refinement of Constancy”  ICTAC 2005: 351-365
[SS05] Stefano Secci, Fausto Spoto “Pair-Sharing Analysis of Object-Oriented Programs” SAS 2005: 320-335
[GS05] Samir Genaim, Fausto Spoto “Information Flow Analysis for Java Bytecode ” VMCAI 2005: 346-362

Contact Us

We're not around right now. But you can send us an email and we'll get back to you, asap.

Start typing and press Enter to search