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.


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

[C32] Pietro Ferrara, Fausto Spoto: Static Analysis for GDPR Compliance. ITASEC 2018

[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

[BCFS25] Gianluca Barbon, Agostino Cortesi, Pietro Ferrara, Enrico Steffinlongo: DAPA: Degradation-Aware Privacy Analysis of Android Apps. STM 2016: 32-46

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

[CFAj2] Giulia Costantini, Pietro Ferrara, Agostino Cortesi: A suite of abstract domains for static analysis of string values. Softw., Pract. Exper. 45(2): 245-287 (2015)
[CFPO20] Agostino Cortesi, Pietro Ferrara, Marco Pistoia, Omer Tripp: Datacentric Semantics for Verification of Privacy Policy Compliance by Mobile Applications. VMCAI 2015: 61-79

[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

[TFM17] Omer Tripp, Pietro Ferrara, Marco Pistoia: Hybrid security analysis of web JavaScript code via dynamic partial evaluation. ISSTA 2014: 49-59
[BFM16] Lucas Brutschy, Pietro Ferrara, Peter Müller: TouchGuru: Integrating Static Analysis with a Mobile Development Environment. MobileDeLi 2014: 33-34
[BFM15] Lucas Brutschy, Pietro Ferrara, Peter Müller: Static analysis for independent app developers. OOPSLA 2014: 847-860
[F14] Pietro Ferrara: Generic Combination of Heap and Value Analyses in Abstract Interpretation. VMCAI 2014: 302-321

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

[Ferr1] Pietro Ferrara: A generic static analyzer for multithreaded Java programs. Softw., Pract. Exper. 43(6): 663-684 (2013)
[CFC12] Agostino Cortesi, Pietro Ferrara, Nabendu Chaki: Static analysis techniques for robotics software verification. ISR 2013: 1-6
[CCF11] Agostino Cortesi, Giulia Costantini, Pietro Ferrara: A Survey on Product Operators in Abstract Interpretation. Festschrift for Dave Schmidt 2013: 325-336

[PS12] Étienne Payet, Fausto Spoto ” Static analysis of Android programs  ” Information & Software Technology 54(11): 1192-1201 (2012 )
[NS12] Durica Nikolic, Fausto Spoto  ” Reachability Analysis of Program Variables ” IJCAR 2012: 423-43 8
[NS12] 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

[ZFC9] Matteo Zanioli, Pietro Ferrara, Agostino Cortesi: SAILS: static analysis of information leakage with sample. SAC 2012: 1308-1313

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

[CFC6] Giulia Costantini, Pietro Ferrara, Agostino Cortesi: Static Analysis of String Values. ICFEM 2011: 505-521

[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-42 4

[Ferr5] Pietro Ferrara: Static Type Analysis of Pattern Matching by Abstract Interpretation. FMOODS/FORTE 2010: 186-200


[PS09] Étienne Payet, Fausto Spoto ” Experiments with Non-Termination Analysis for Java Bytecode. Electr. Notes Theor ”  Comput. Sci. 253(5): 83-9 6

[SLM09] Fausto Spoto, Lunjin Lu, Fred Mesnard ”  Using CLP Simplifications to Improve Java Bytecode Termintion Analysis. Electr. Notes. Theor. Comput ”  Sci. 253(5): 129-144

[Ferr1] Pietro Ferrara: Static analysis via abstract interpretation of multithreaded programs. (Analyse statique de logiciels MultitâCHES par InterpréTation abstraite). École Polytechnique, Palaiseau, France 2009
[Ferr4] Pietro Ferrara: Checkmate: A Generic Static Analyzer of Java Multithreaded Programs. SEFM 2009: 169-178

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

[Ferr2Pietro Ferrara: Static Analysis of the Determinism of Multithreaded Programs. SEFM 2008: 41-50

[Ferr1]  Pietro Ferrara: Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model. TAP 2008: 116-



[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


[HS06] 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