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.


[AFK20] A. Mandal, P. Ferrara, Y. Khlyebnikov, A. Cortesi, F. Spoto: “Cross-Program Taint Analysis for IoT Systems”, Proceedings of the 35th ACM Symposium on Applied Computing (SAC 2020), ACM Press, Brno, Czech Republic, March 30-April 3, 2020

[FOS20] P. Ferrara, L. Olivieri, F. Spoto: “BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results”, Proceedings of the 21th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2020), LNCS, Springer, New Orleans, United States, January 19-21, 2020


[FMCb19] P. Ferrara, A. Mandal, A. Cortesi, F. Spoto: “Cross-Programming Language Taint Analysis for the IoT Ecosystem”, Electronic Communication of the European Association of Software Science and Technology, Volume 77, October 2019

[SBE19] F. Spoto, E. Burato, M. D. Ernst, P. Ferrara, A. Lovato, D. Macedonio, C. Spiridon: “Static Identification of Injection Attacks in Java”, ACM Transactions on Programming Languages and Systems, Volume 41 Issue 3, July 2019

[MPC19] A. Mandal, F. Panarotto, A. Cortesi, P. Ferrara, F. Spoto, “Static Analysis of Android Auto Infotainment and ODB-II Apps”, Software: Practice and Experience, Volume 49, Issue 7, Pages 1131-1161, July 2019

[FMCa19] P. Ferrara, A. Mandal, A. Cortesi, F. Spoto: “Static Analysis for the OWASP IoT Top 10 2018”, Workshop on Security practices for Internet of Things (SPIoT 2019), Prague, Czech Republic, April 7, 2019

[FMC19] P. Ferrara, A. Mandal, A. Cortesi, F. Spoto: “Cross Programming Language Taint Analysis for the IoT Ecosystem”, Interactive Workshop on the Industrial Application of Verification and Testing (InterAVT 2019), Prague, Czech Republic, April 6, 2019

[FA19] P. Ferrara, P. Anderson: “Semantic Static Analysis of IoT Software”, Proceedings of Embedded World 2019, Nuremberg, Germany, February 26-28, 2019


[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


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


[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


[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 )


[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


[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


[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


[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


[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


[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


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


[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


[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)


[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