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


We use cookies to offer you the best online experience. Accepting the acceptance of cookies in accordance with our cookie policy.

I accept I decline Centro Privacy Impostazioni della Privacy Learn More about our Cookie Policy