Visible to the public Synthesis of a Complex Software Vulnerability Analyzer (SVA)